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  3212  unidif  3776  iunxdif2  3869  exss  4157  reg2exmidlema  4457  limom  4535  xpiindim  4684  relssres  4865  funco  5171  nfunsn  5463  fliftcnv  5704  fo1stresm  6067  fo2ndresm  6068  dftpos3  6167  tfri1d  6240  rdgtfr  6279  rdgruledefgg  6280  frectfr  6305  elixpsn  6637  mapxpen  6750  phplem2  6755  sbthlem2  6854  sbthlemi3  6855  djuss  6963  caseinl  6984  caseinr  6985  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  nqprrnd  7375  nqprxx  7378  ltexprlempr  7440  recexprlempr  7464  cauappcvgprlemcl  7485  caucvgprlemcl  7508  caucvgprprlemcl  7536  suplocsrlempr  7639  lemulge11  8648  nn0ge2m1nn  9061  frecfzennn  10230  reccn2ap  11114  demoivreALT  11516  topcld  12317  metrest  12714  pwle2  13366