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  3336  unidif  3923  iunxdif2  4017  exss  4317  reg2exmidlema  4630  limom  4710  xpiindim  4865  relssres  5049  funco  5364  nfunsn  5672  fliftcnv  5931  fo1stresm  6319  fo2ndresm  6320  dftpos3  6423  tfri1d  6496  rdgtfr  6535  rdgruledefgg  6536  frectfr  6561  elixpsn  6899  mapxpen  7029  phplem2  7034  sbthlem2  7148  sbthlemi3  7149  djuss  7260  caseinl  7281  caseinr  7282  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  2omotaplemap  7466  nqprrnd  7753  nqprxx  7756  ltexprlempr  7818  recexprlempr  7842  cauappcvgprlemcl  7863  caucvgprlemcl  7886  caucvgprprlemcl  7914  suplocsrlempr  8017  lemulge11  9036  nn0ge2m1nn  9452  frecfzennn  10678  wrdlenge2n0  11139  swrdnd  11230  reccn2ap  11864  demoivreALT  12325  pcdiv  12865  idghm  13836  subrgid  14227  mulgghm2  14612  topcld  14823  metrest  15220  2lgs  15823  pwle2  16535