Theorem jctil 312

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 306	1 |- ( ph -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  jctl  314  ddifnel  3338  unidif  3925  iunxdif2  4019  exss  4319  reg2exmidlema  4632  limom  4712  xpiindim  4867  relssres  5051  funco  5366  nfunsn  5676  fliftcnv  5935  fo1stresm  6323  fo2ndresm  6324  dftpos3  6427  tfri1d  6500  rdgtfr  6539  rdgruledefgg  6540  frectfr  6565  elixpsn  6903  mapxpen  7033  phplem2  7038  sbthlem2  7156  sbthlemi3  7157  djuss  7268  caseinl  7289  caseinr  7290  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  2omotaplemap  7475  nqprrnd  7762  nqprxx  7765  ltexprlempr  7827  recexprlempr  7851  cauappcvgprlemcl  7872  caucvgprlemcl  7895  caucvgprprlemcl  7923  suplocsrlempr  8026  lemulge11  9045  nn0ge2m1nn  9461  frecfzennn  10687  wrdlenge2n0  11148  swrdnd  11239  reccn2ap  11873  demoivreALT  12334  pcdiv  12874  idghm  13845  subrgid  14236  mulgghm2  14621  topcld  14832  metrest  15229  2lgs  15832  pwle2  16599