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  3207  unidif  3768  iunxdif2  3861  exss  4149  reg2exmidlema  4449  limom  4527  xpiindim  4676  relssres  4857  funco  5163  nfunsn  5455  fliftcnv  5696  fo1stresm  6059  fo2ndresm  6060  dftpos3  6159  tfri1d  6232  rdgtfr  6271  rdgruledefgg  6272  frectfr  6297  elixpsn  6629  mapxpen  6742  phplem2  6747  sbthlem2  6846  sbthlemi3  6847  djuss  6955  caseinl  6976  caseinr  6977  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  nqprrnd  7351  nqprxx  7354  ltexprlempr  7416  recexprlempr  7440  cauappcvgprlemcl  7461  caucvgprlemcl  7484  caucvgprprlemcl  7512  suplocsrlempr  7615  lemulge11  8624  nn0ge2m1nn  9037  frecfzennn  10199  reccn2ap  11082  demoivreALT  11480  topcld  12278  metrest  12675  pwle2  13193