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  3304  unidif  3882  iunxdif2  3976  exss  4271  reg2exmidlema  4582  limom  4662  xpiindim  4815  relssres  4997  funco  5311  nfunsn  5611  fliftcnv  5864  fo1stresm  6247  fo2ndresm  6248  dftpos3  6348  tfri1d  6421  rdgtfr  6460  rdgruledefgg  6461  frectfr  6486  elixpsn  6822  mapxpen  6945  phplem2  6950  sbthlem2  7060  sbthlemi3  7061  djuss  7172  caseinl  7193  caseinr  7194  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  2omotaplemap  7369  nqprrnd  7656  nqprxx  7659  ltexprlempr  7721  recexprlempr  7745  cauappcvgprlemcl  7766  caucvgprlemcl  7789  caucvgprprlemcl  7817  suplocsrlempr  7920  lemulge11  8939  nn0ge2m1nn  9355  frecfzennn  10571  wrdlenge2n0  11029  swrdnd  11112  reccn2ap  11624  demoivreALT  12085  pcdiv  12625  idghm  13595  subrgid  13985  mulgghm2  14370  topcld  14581  metrest  14978  2lgs  15581  pwle2  15935