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  3267  unidif  3842  iunxdif2  3936  exss  4228  reg2exmidlema  4534  limom  4614  xpiindim  4765  relssres  4946  funco  5257  nfunsn  5550  fliftcnv  5796  fo1stresm  6162  fo2ndresm  6163  dftpos3  6263  tfri1d  6336  rdgtfr  6375  rdgruledefgg  6376  frectfr  6401  elixpsn  6735  mapxpen  6848  phplem2  6853  sbthlem2  6957  sbthlemi3  6958  djuss  7069  caseinl  7090  caseinr  7091  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  2omotaplemap  7256  nqprrnd  7542  nqprxx  7545  ltexprlempr  7607  recexprlempr  7631  cauappcvgprlemcl  7652  caucvgprlemcl  7675  caucvgprprlemcl  7703  suplocsrlempr  7806  lemulge11  8823  nn0ge2m1nn  9236  frecfzennn  10426  reccn2ap  11321  demoivreALT  11781  pcdiv  12302  subrgid  13344  topcld  13612  metrest  14009  pwle2  14751