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  9198  nn0ge2m1nn  9631  frecfzennn  10876  hashfibclem  11296  wrdlenge2n0  11354  swrdnd  11445  reccn2ap  12095  demoivreALT  12557  pcdiv  13101  ballotfilemfc0  13281  ballotfilemfcc  13282  idghm  14111  subrgid  14580  mulgghm2  14992  topcld  15259  metrest  15656  2lgs  16321  pwle2  17126