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  3290  unidif  3867  iunxdif2  3961  exss  4256  reg2exmidlema  4566  limom  4646  xpiindim  4799  relssres  4980  funco  5294  nfunsn  5589  fliftcnv  5838  fo1stresm  6214  fo2ndresm  6215  dftpos3  6315  tfri1d  6388  rdgtfr  6427  rdgruledefgg  6428  frectfr  6453  elixpsn  6789  mapxpen  6904  phplem2  6909  sbthlem2  7017  sbthlemi3  7018  djuss  7129  caseinl  7150  caseinr  7151  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  2omotaplemap  7317  nqprrnd  7603  nqprxx  7606  ltexprlempr  7668  recexprlempr  7692  cauappcvgprlemcl  7713  caucvgprlemcl  7736  caucvgprprlemcl  7764  suplocsrlempr  7867  lemulge11  8885  nn0ge2m1nn  9300  frecfzennn  10497  wrdlenge2n0  10949  reccn2ap  11456  demoivreALT  11917  pcdiv  12440  idghm  13329  subrgid  13719  mulgghm2  14096  topcld  14277  metrest  14674  pwle2  15489