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  3337  unidif  3924  iunxdif2  4018  exss  4318  reg2exmidlema  4631  limom  4711  xpiindim  4866  relssres  5050  funco  5365  nfunsn  5676  fliftcnv  5938  fo1stresm  6326  fo2ndresm  6327  dftpos3  6430  tfri1d  6503  rdgtfr  6542  rdgruledefgg  6543  frectfr  6568  elixpsn  6906  mapxpen  7036  phplem2  7041  sbthlem2  7159  sbthlemi3  7160  djuss  7271  caseinl  7292  caseinr  7293  exmidfodomrlemr  7415  exmidfodomrlemrALT  7416  2omotaplemap  7478  nqprrnd  7765  nqprxx  7768  ltexprlempr  7830  recexprlempr  7854  cauappcvgprlemcl  7875  caucvgprlemcl  7898  caucvgprprlemcl  7926  suplocsrlempr  8029  lemulge11  9048  nn0ge2m1nn  9464  frecfzennn  10691  wrdlenge2n0  11155  swrdnd  11246  reccn2ap  11893  demoivreALT  12355  pcdiv  12895  idghm  13866  subrgid  14258  mulgghm2  14643  topcld  14859  metrest  15256  2lgs  15859  pwle2  16657