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  3291  unidif  3868  iunxdif2  3962  exss  4257  reg2exmidlema  4567  limom  4647  xpiindim  4800  relssres  4981  funco  5295  nfunsn  5590  fliftcnv  5839  fo1stresm  6216  fo2ndresm  6217  dftpos3  6317  tfri1d  6390  rdgtfr  6429  rdgruledefgg  6430  frectfr  6455  elixpsn  6791  mapxpen  6906  phplem2  6911  sbthlem2  7019  sbthlemi3  7020  djuss  7131  caseinl  7152  caseinr  7153  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  2omotaplemap  7319  nqprrnd  7605  nqprxx  7608  ltexprlempr  7670  recexprlempr  7694  cauappcvgprlemcl  7715  caucvgprlemcl  7738  caucvgprprlemcl  7766  suplocsrlempr  7869  lemulge11  8887  nn0ge2m1nn  9303  frecfzennn  10500  wrdlenge2n0  10952  reccn2ap  11459  demoivreALT  11920  pcdiv  12443  idghm  13332  subrgid  13722  mulgghm2  14107  topcld  14288  metrest  14685  2lgs  15261  pwle2  15559