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  3360  unidif  3962  iunxdif2  4056  exss  4362  reg2exmidlema  4676  limom  4756  xpiindim  4912  relssres  5096  funco  5412  nfunsn  5727  fliftcnv  5991  fo1stresm  6385  fo2ndresm  6386  dftpos3  6523  tfri1d  6596  rdgtfr  6635  rdgruledefgg  6636  frectfr  6661  elixpsn  7007  mapxpen  7138  phplem2  7144  sbthlem2  7265  sbthlemi3  7266  djuss  7400  caseinl  7421  caseinr  7422  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  2omotaplemap  7613  nqprrnd  7900  nqprxx  7903  ltexprlempr  7965  recexprlempr  7989  cauappcvgprlemcl  8010  caucvgprlemcl  8033  caucvgprprlemcl  8061  suplocsrlempr  8164  lemulge11  9186  nn0ge2m1nn  9606  frecfzennn  10841  hashfibclem  11260  wrdlenge2n0  11318  swrdnd  11409  reccn2ap  12057  demoivreALT  12519  pcdiv  13059  ballotfilemfc0  13210  ballotfilemfcc  13211  idghm  14039  subrgid  14504  mulgghm2  14915  topcld  15133  metrest  15530  2lgs  16137  pwle2  16942