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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jctl  314  ddifnel  3360  unidif  3967  iunxdif2  4061  exss  4369  reg2exmidlema  4683  limom  4763  xpiindim  4919  relssres  5103  funco  5420  nfunsn  5736  fliftcnv  6004  fo1stresm  6399  fo2ndresm  6400  dftpos3  6538  tfri1d  6611  rdgtfr  6650  rdgruledefgg  6651  frectfr  6676  elixpsn  7023  mapxpen  7154  phplem2  7160  sbthlem2  7282  sbthlemi3  7283  djuss  7416  caseinl  7437  caseinr  7438  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  2omotaplemap  7629  nqprrnd  7916  nqprxx  7919  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocsrlempr  8180  lemulge11  9204  nn0ge2m1nn  9636  frecfzennn  10883  hashfibclem  11303  wrdlenge2n0  11361  swrdnd  11452  reccn2ap  12103  demoivreALT  12565  pcdiv  13109  ballotfilemfc0  13289  ballotfilemfcc  13290  idghm  14120  subrgid  14639  mulgghm2  15051  psrbagmax  15183  topcld  15352  metrest  15749  2lgs  16445  pwle2  17250