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  3335  unidif  3920  iunxdif2  4014  exss  4313  reg2exmidlema  4626  limom  4706  xpiindim  4859  relssres  5043  funco  5358  nfunsn  5664  fliftcnv  5919  fo1stresm  6307  fo2ndresm  6308  dftpos3  6408  tfri1d  6481  rdgtfr  6520  rdgruledefgg  6521  frectfr  6546  elixpsn  6882  mapxpen  7009  phplem2  7014  sbthlem2  7125  sbthlemi3  7126  djuss  7237  caseinl  7258  caseinr  7259  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  2omotaplemap  7443  nqprrnd  7730  nqprxx  7733  ltexprlempr  7795  recexprlempr  7819  cauappcvgprlemcl  7840  caucvgprlemcl  7863  caucvgprprlemcl  7891  suplocsrlempr  7994  lemulge11  9013  nn0ge2m1nn  9429  frecfzennn  10648  wrdlenge2n0  11107  swrdnd  11191  reccn2ap  11824  demoivreALT  12285  pcdiv  12825  idghm  13796  subrgid  14187  mulgghm2  14572  topcld  14783  metrest  15180  2lgs  15783  pwle2  16364