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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jctl  314  ddifnel  3360  unidif  3967  iunxdif2  4061  exss  4367  reg2exmidlema  4681  limom  4761  xpiindim  4917  relssres  5101  funco  5417  nfunsn  5733  fliftcnv  6001  fo1stresm  6395  fo2ndresm  6396  dftpos3  6533  tfri1d  6606  rdgtfr  6645  rdgruledefgg  6646  frectfr  6671  elixpsn  7017  mapxpen  7148  phplem2  7154  sbthlem2  7275  sbthlemi3  7276  djuss  7411  caseinl  7432  caseinr  7433  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  2omotaplemap  7624  nqprrnd  7911  nqprxx  7914  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  caucvgprlemcl  8044  caucvgprprlemcl  8072  suplocsrlempr  8175  lemulge11  9199  nn0ge2m1nn  9632  frecfzennn  10878  hashfibclem  11298  wrdlenge2n0  11356  swrdnd  11447  reccn2ap  12098  demoivreALT  12560  pcdiv  13104  ballotfilemfc0  13284  ballotfilemfcc  13285  idghm  14115  subrgid  14615  mulgghm2  15027  topcld  15301  metrest  15698  2lgs  16389  pwle2  17194