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  3335  unidif  3920  iunxdif2  4014  exss  4313  reg2exmidlema  4626  limom  4706  xpiindim  4859  relssres  5043  funco  5358  nfunsn  5666  fliftcnv  5925  fo1stresm  6313  fo2ndresm  6314  dftpos3  6414  tfri1d  6487  rdgtfr  6526  rdgruledefgg  6527  frectfr  6552  elixpsn  6890  mapxpen  7017  phplem2  7022  sbthlem2  7136  sbthlemi3  7137  djuss  7248  caseinl  7269  caseinr  7270  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  2omotaplemap  7454  nqprrnd  7741  nqprxx  7744  ltexprlempr  7806  recexprlempr  7830  cauappcvgprlemcl  7851  caucvgprlemcl  7874  caucvgprprlemcl  7902  suplocsrlempr  8005  lemulge11  9024  nn0ge2m1nn  9440  frecfzennn  10660  wrdlenge2n0  11120  swrdnd  11207  reccn2ap  11840  demoivreALT  12301  pcdiv  12841  idghm  13812  subrgid  14203  mulgghm2  14588  topcld  14799  metrest  15196  2lgs  15799  pwle2  16451