Theorem jctil 310

Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

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 9	. 2 |- ( ph -> ch )
3		jctil.1	. 2 |- ( ph -> ps )
4	2, 3	jca 304	1 |- ( ph -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jctl  312  ddifnel  3252  unidif  3820  iunxdif2  3913  exss  4204  reg2exmidlema  4510  limom  4590  xpiindim  4740  relssres  4921  funco  5227  nfunsn  5519  fliftcnv  5762  fo1stresm  6126  fo2ndresm  6127  dftpos3  6226  tfri1d  6299  rdgtfr  6338  rdgruledefgg  6339  frectfr  6364  elixpsn  6697  mapxpen  6810  phplem2  6815  sbthlem2  6919  sbthlemi3  6920  djuss  7031  caseinl  7052  caseinr  7053  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  nqprrnd  7480  nqprxx  7483  ltexprlempr  7545  recexprlempr  7569  cauappcvgprlemcl  7590  caucvgprlemcl  7613  caucvgprprlemcl  7641  suplocsrlempr  7744  lemulge11  8757  nn0ge2m1nn  9170  frecfzennn  10357  reccn2ap  11250  demoivreALT  11710  pcdiv  12230  topcld  12709  metrest  13106  pwle2  13838