Theorem syl5 28

Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	|- (ph -> ps)
syl5.2	|- (ch -> (ps -> th))

Assertion

Ref	Expression
syl5	|- (ch -> (ph -> th))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 |- (ph -> ps)
2		syl5.2	. . 3 |- (ch -> (ps -> th))
3	1, 2	syl5com 26	. 2 |- (ph -> (ch -> th))
4	3	com12 27	1 |- (ch -> (ph -> th))

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl56  30  syl2im  34  imim12i  53  pm2.86d  93  con2d  107  con3d  125  nsyli  133  syl5bi  208  syl5bir  209  syl5ib  210  adantld  453  adantrd  454  mpan9  455  pm4.79  566  pm2.36  816  pm4.72  846  ecased  910  ecase3ad  911  syl3an2  1216  alrimdh  1587  ax11w  1721  ax12dgen2  1726  ax5o  1749  spsd  1755  hbnt  1775  nfndOLD  1792  stdpc5OLD  1799  19.21hOLD  1840  cbv3hvOLD  1851  ax12olem5  1931  a16g  1945  hbae  1953  dvelimh  1964  exdistrf  1971  ax11a2  1993  sbft  2025  sbied  2036  sb4  2053  ax11v  2096  ax11vALT  2097  ax5  2146  hbae-o  2153  dvelimf-o  2180  ax11indn  2195  ax11inda2  2199  ax11a2-o  2202  euimmo  2253  mopick  2266  spcimgft  2930  rr19.28v  2981  moeq3  3013  mob2  3016  euind  3023  reuind  3039  sbeqalb  3098  sbcimdv  3107  csbexg  3146  opkthg  4131  nndisjeq  4429  sfin112  4529  sfintfin  4532  sfinltfin  4535  vfinspsslem1  4550  vfinspss  4551  phi11lem1  4595  copsexg  4607  dmcosseq  4973  ssreseq  4997  dfco2a  5081  imadif  5171  dff4  5421  foco2  5426  funfvima2  5460  oprabid  5550  ovmpt4g  5710  ov2gf  5711  fvmptf  5722  fvmptnf  5723  clos1conn  5879  connexd  5931  ectocld  5991  enmap2lem3  6065  enmap1lem3  6071  enprmaplem3  6078  enprmaplem5  6080  enprmaplem6  6081  ncdisjun  6136  nceleq  6149  peano4nc  6150  ncssfin  6151  fce  6188  lectr  6211  leltctr  6212  taddc  6229  tlecg  6230  nclenn  6249  addcdi  6250  ncslesuc  6267  nchoicelem9  6297  nchoicelem15  6303  nchoicelem17  6305  dmfrec  6316  fnfreclem3  6319  fnfrec  6320