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  4367  reg2exmidlema  4681  limom  4761  xpiindim  4917  relssres  5101  funco  5417  nfunsn  5733  fliftcnv  6001  fo1stresm  6395  fo2ndresm  6396  dftpos3  6533  tfri1d  6606  rdgtfr  6645  rdgruledefgg  6646  frectfr  6671  elixpsn  7017  mapxpen  7148  phplem2  7154  sbthlem2  7275  sbthlemi3  7276  djuss  7410  caseinl  7431  caseinr  7432  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  2omotaplemap  7623  nqprrnd  7910  nqprxx  7913  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocsrlempr  8174  lemulge11  9196  nn0ge2m1nn  9627  frecfzennn  10863  hashfibclem  11282  wrdlenge2n0  11340  swrdnd  11431  reccn2ap  12079  demoivreALT  12541  pcdiv  13081  ballotfilemfc0  13232  ballotfilemfcc  13233  idghm  14062  subrgid  14531  mulgghm2  14943  topcld  15210  metrest  15607  2lgs  16223  pwle2  17028