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  7281  exmidfodomrlemrALT  7282  2omotaplemap  7340  nqprrnd  7627  nqprxx  7630  ltexprlempr  7692  recexprlempr  7716  cauappcvgprlemcl  7737  caucvgprlemcl  7760  caucvgprprlemcl  7788  suplocsrlempr  7891  lemulge11  8910  nn0ge2m1nn  9326  frecfzennn  10535  wrdlenge2n0  10987  reccn2ap  11495  demoivreALT  11956  pcdiv  12496  idghm  13465  subrgid  13855  mulgghm2  14240  topcld  14429  metrest  14826  2lgs  15429  pwle2  15729