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  3312  unidif  3896  iunxdif2  3990  exss  4289  reg2exmidlema  4600  limom  4680  xpiindim  4833  relssres  5016  funco  5330  nfunsn  5634  fliftcnv  5887  fo1stresm  6270  fo2ndresm  6271  dftpos3  6371  tfri1d  6444  rdgtfr  6483  rdgruledefgg  6484  frectfr  6509  elixpsn  6845  mapxpen  6970  phplem2  6975  sbthlem2  7086  sbthlemi3  7087  djuss  7198  caseinl  7219  caseinr  7220  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  2omotaplemap  7404  nqprrnd  7691  nqprxx  7694  ltexprlempr  7756  recexprlempr  7780  cauappcvgprlemcl  7801  caucvgprlemcl  7824  caucvgprprlemcl  7852  suplocsrlempr  7955  lemulge11  8974  nn0ge2m1nn  9390  frecfzennn  10608  wrdlenge2n0  11066  swrdnd  11150  reccn2ap  11739  demoivreALT  12200  pcdiv  12740  idghm  13710  subrgid  14100  mulgghm2  14485  topcld  14696  metrest  15093  2lgs  15696  pwle2  16137