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  3350  unidif  3946  iunxdif2  4040  exss  4343  reg2exmidlema  4656  limom  4736  xpiindim  4892  relssres  5076  funco  5392  nfunsn  5707  fliftcnv  5968  fo1stresm  6355  fo2ndresm  6356  dftpos3  6493  tfri1d  6566  rdgtfr  6605  rdgruledefgg  6606  frectfr  6631  elixpsn  6970  mapxpen  7101  phplem2  7107  sbthlem2  7228  sbthlemi3  7229  djuss  7361  caseinl  7382  caseinr  7383  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  2omotaplemap  7571  nqprrnd  7858  nqprxx  7861  ltexprlempr  7923  recexprlempr  7947  cauappcvgprlemcl  7968  caucvgprlemcl  7991  caucvgprprlemcl  8019  suplocsrlempr  8122  lemulge11  9140  nn0ge2m1nn  9560  frecfzennn  10788  hashfibclem  11206  wrdlenge2n0  11260  swrdnd  11351  reccn2ap  11998  demoivreALT  12460  pcdiv  13000  idghm  13976  subrgid  14368  mulgghm2  14756  topcld  14974  metrest  15371  2lgs  15977  pwle2  16772