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  3258  unidif  3828  iunxdif2  3921  exss  4212  reg2exmidlema  4518  limom  4598  xpiindim  4748  relssres  4929  funco  5238  nfunsn  5530  fliftcnv  5774  fo1stresm  6140  fo2ndresm  6141  dftpos3  6241  tfri1d  6314  rdgtfr  6353  rdgruledefgg  6354  frectfr  6379  elixpsn  6713  mapxpen  6826  phplem2  6831  sbthlem2  6935  sbthlemi3  6936  djuss  7047  caseinl  7068  caseinr  7069  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  nqprrnd  7505  nqprxx  7508  ltexprlempr  7570  recexprlempr  7594  cauappcvgprlemcl  7615  caucvgprlemcl  7638  caucvgprprlemcl  7666  suplocsrlempr  7769  lemulge11  8782  nn0ge2m1nn  9195  frecfzennn  10382  reccn2ap  11276  demoivreALT  11736  pcdiv  12256  topcld  12903  metrest  13300  pwle2  14031