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  3304  unidif  3882  iunxdif2  3976  exss  4272  reg2exmidlema  4583  limom  4663  xpiindim  4816  relssres  4998  funco  5312  nfunsn  5613  fliftcnv  5866  fo1stresm  6249  fo2ndresm  6250  dftpos3  6350  tfri1d  6423  rdgtfr  6462  rdgruledefgg  6463  frectfr  6488  elixpsn  6824  mapxpen  6947  phplem2  6952  sbthlem2  7062  sbthlemi3  7063  djuss  7174  caseinl  7195  caseinr  7196  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  2omotaplemap  7371  nqprrnd  7658  nqprxx  7661  ltexprlempr  7723  recexprlempr  7747  cauappcvgprlemcl  7768  caucvgprlemcl  7791  caucvgprprlemcl  7819  suplocsrlempr  7922  lemulge11  8941  nn0ge2m1nn  9357  frecfzennn  10573  wrdlenge2n0  11031  swrdnd  11115  reccn2ap  11657  demoivreALT  12118  pcdiv  12658  idghm  13628  subrgid  14018  mulgghm2  14403  topcld  14614  metrest  15011  2lgs  15614  pwle2  15972