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  4369  reg2exmidlema  4683  limom  4763  xpiindim  4919  relssres  5103  funco  5420  nfunsn  5736  fliftcnv  6004  fo1stresm  6399  fo2ndresm  6400  dftpos3  6537  tfri1d  6610  rdgtfr  6649  rdgruledefgg  6650  frectfr  6675  elixpsn  7021  mapxpen  7152  phplem2  7158  sbthlem2  7280  sbthlemi3  7281  djuss  7416  caseinl  7437  caseinr  7438  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  2omotaplemap  7629  nqprrnd  7916  nqprxx  7919  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocsrlempr  8180  lemulge11  9204  nn0ge2m1nn  9638  frecfzennn  10884  hashfibclem  11304  wrdlenge2n0  11362  swrdnd  11453  reccn2ap  12104  demoivreALT  12566  pcdiv  13110  ballotfilemfc0  13290  ballotfilemfcc  13291  idghm  14121  subrgid  14640  mulgghm2  15052  topcld  15335  metrest  15732  2lgs  16428  pwle2  17233