Theorem jctil 310

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 304	1 |- ( ph -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jctl  312  ddifnel  3238  unidif  3804  iunxdif2  3897  exss  4186  reg2exmidlema  4491  limom  4571  xpiindim  4720  relssres  4901  funco  5207  nfunsn  5499  fliftcnv  5740  fo1stresm  6103  fo2ndresm  6104  dftpos3  6203  tfri1d  6276  rdgtfr  6315  rdgruledefgg  6316  frectfr  6341  elixpsn  6673  mapxpen  6786  phplem2  6791  sbthlem2  6895  sbthlemi3  6896  djuss  7004  caseinl  7025  caseinr  7026  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  nqprrnd  7446  nqprxx  7449  ltexprlempr  7511  recexprlempr  7535  cauappcvgprlemcl  7556  caucvgprlemcl  7579  caucvgprprlemcl  7607  suplocsrlempr  7710  lemulge11  8720  nn0ge2m1nn  9133  frecfzennn  10307  reccn2ap  11192  demoivreALT  11652  topcld  12469  metrest  12866  pwle2  13531