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  3295  unidif  3872  iunxdif2  3966  exss  4261  reg2exmidlema  4571  limom  4651  xpiindim  4804  relssres  4985  funco  5299  nfunsn  5596  fliftcnv  5845  fo1stresm  6228  fo2ndresm  6229  dftpos3  6329  tfri1d  6402  rdgtfr  6441  rdgruledefgg  6442  frectfr  6467  elixpsn  6803  mapxpen  6918  phplem2  6923  sbthlem2  7033  sbthlemi3  7034  djuss  7145  caseinl  7166  caseinr  7167  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  2omotaplemap  7342  nqprrnd  7629  nqprxx  7632  ltexprlempr  7694  recexprlempr  7718  cauappcvgprlemcl  7739  caucvgprlemcl  7762  caucvgprprlemcl  7790  suplocsrlempr  7893  lemulge11  8912  nn0ge2m1nn  9328  frecfzennn  10537  wrdlenge2n0  10989  reccn2ap  11497  demoivreALT  11958  pcdiv  12498  idghm  13467  subrgid  13857  mulgghm2  14242  topcld  14453  metrest  14850  2lgs  15453  pwle2  15753