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  3340  unidif  3930  iunxdif2  4024  exss  4325  reg2exmidlema  4638  limom  4718  xpiindim  4873  relssres  5057  funco  5373  nfunsn  5685  fliftcnv  5946  fo1stresm  6333  fo2ndresm  6334  dftpos3  6471  tfri1d  6544  rdgtfr  6583  rdgruledefgg  6584  frectfr  6609  elixpsn  6947  mapxpen  7077  phplem2  7082  sbthlem2  7200  sbthlemi3  7201  djuss  7329  caseinl  7350  caseinr  7351  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  2omotaplemap  7536  nqprrnd  7823  nqprxx  7826  ltexprlempr  7888  recexprlempr  7912  cauappcvgprlemcl  7933  caucvgprlemcl  7956  caucvgprprlemcl  7984  suplocsrlempr  8087  lemulge11  9105  nn0ge2m1nn  9523  frecfzennn  10751  wrdlenge2n0  11215  swrdnd  11306  reccn2ap  11953  demoivreALT  12415  pcdiv  12955  idghm  13926  subrgid  14318  mulgghm2  14704  topcld  14920  metrest  15317  2lgs  15923  pwle2  16720