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  3266  unidif  3841  iunxdif2  3935  exss  4227  reg2exmidlema  4533  limom  4613  xpiindim  4764  relssres  4945  funco  5256  nfunsn  5549  fliftcnv  5795  fo1stresm  6161  fo2ndresm  6162  dftpos3  6262  tfri1d  6335  rdgtfr  6374  rdgruledefgg  6375  frectfr  6400  elixpsn  6734  mapxpen  6847  phplem2  6852  sbthlem2  6956  sbthlemi3  6957  djuss  7068  caseinl  7089  caseinr  7090  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  2omotaplemap  7255  nqprrnd  7541  nqprxx  7544  ltexprlempr  7606  recexprlempr  7630  cauappcvgprlemcl  7651  caucvgprlemcl  7674  caucvgprprlemcl  7702  suplocsrlempr  7805  lemulge11  8822  nn0ge2m1nn  9235  frecfzennn  10425  reccn2ap  11320  demoivreALT  11780  pcdiv  12301  subrgid  13342  topcld  13579  metrest  13976  pwle2  14718