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  3354  unidif  3951  iunxdif2  4045  exss  4348  reg2exmidlema  4661  limom  4741  xpiindim  4897  relssres  5081  funco  5397  nfunsn  5712  fliftcnv  5974  fo1stresm  6368  fo2ndresm  6369  dftpos3  6506  tfri1d  6579  rdgtfr  6618  rdgruledefgg  6619  frectfr  6644  elixpsn  6983  mapxpen  7114  phplem2  7120  sbthlem2  7241  sbthlemi3  7242  djuss  7374  caseinl  7395  caseinr  7396  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  2omotaplemap  7587  nqprrnd  7874  nqprxx  7877  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  caucvgprlemcl  8007  caucvgprprlemcl  8035  suplocsrlempr  8138  lemulge11  9157  nn0ge2m1nn  9577  frecfzennn  10812  hashfibclem  11231  wrdlenge2n0  11285  swrdnd  11376  reccn2ap  12023  demoivreALT  12485  pcdiv  13025  ballotfilemfc0  13176  ballotfilemfcc  13177  idghm  14012  subrgid  14469  mulgghm2  14882  topcld  15100  metrest  15497  2lgs  16103  pwle2  16898