Theorem jctil 240

Description: Inference conjoining a theorem to left of consequent in an implication.

Hypotheses

Ref	Expression
jctil.1	|- (ph -> ps)
jctil.2	|- ch

Assertion

Ref	Expression
jctil	|- (ph -> (ch /\ ps))

Proof of Theorem jctil

Step	Hyp	Ref	Expression
1		jctil.2	. . 3 |- ch
2	1	a1i 7	. 2 |- (ph -> ch)
3		jctil.1	. 2 |- (ph -> ps)
4	2, 3	jca 236	1 |- (ph -> (ch /\ ps))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  exss 1881  unidif 1943  intmin 1982  frirr 2176  unon 2338  onuninsuc 2356  limom 2387  dmcosseq 2572  relssres 2596  funco 2696  funssres 2698  fconst 2774  fconst2 2902  f1oweOLD 2944  oawordeulem 3156  undom 3342  sbthlem2 3350  sbthlem3 3351  sbthlem8 3356  phplem3 3405  pssnn 3428  inf3lem6 3469  kmlem1 3580  cflim 3704  cfsuc 3709  reclem2pr 3951  suplem2pr 3956  supsrlem2 4020  axrecex 4079  divge0 4392  posex 4422  nnge1t 4439  nnsub 4450  nnaddm1clt 4452  nnreclt 4522  discrlem3 4715  sqrlem17 4747  clim0 4882  ruclem8 4892  infdif 4948  hiidge0t 5056  his6 5057  norm-it 5080  bcs 5101  hlim0 5140  hlimcaui 5141  ocsh 5164  occllem6 5185  projlem2 5194  projlem12 5204  projlem13 5205  projlem26 5218  projlem28 5220  pjthlem10 5234  pjthlem12 5236  pjthlem14 5238  ococint 5298  hsupval2t 5301  spanclt 5305  hsupclt 5308  chabs2t 5433  pjoml5 5498  osum 5538  pjss2 5571  pjssm 5572  stle 5681  strlem1 5691  atcvat3 5774  atcvat4 5775  sumdmd 5787

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org