Theorem syl5 21

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise.

Hypotheses

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

Assertion

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

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. 2 |- (ph -> (ps -> ch))
2		syl5.2	. . 3 |- (th -> ps)
3	2	imim1i 16	. 2 |- ((ps -> ch) -> (th -> ch))
4	1, 3	syl 10	1 |- (ph -> (th -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.04 30  nsyli 121  syl5ib 206  syl5ibr 207  syl5bi 208  syl5bir 210  jao 340  adantrd 391  sylan2 451  pm2.36 570  pm5.18 660  elimant 684  prlem1 770  syl3an2 860  meredith 924  ax4 972  ax5o 974  ax5 976  a4sd 985  hbnt 1002  19.21 1056  equtr2 1133  hbae 1145  dvelimfALT 1153  cbv2 1163  sbied 1195  ax11a2 1216  sb4 1223  hbsb4 1248  ax11v 1265  ax11indn 1366  ax11inda2 1370  a12study 1378  hbeu 1389  euimmo 1420  mopick 1433  moeq3 1921  sbcbid 1976  sbc19.20dv 1985  ra4sbc 1997  csbexg 2008  csbeq2d 2018  pwssun 2827  reuuni4 2887  ralxfr 2899  wereu 2945  tz7.7 2973  onfr 2986  ordtr2 3002  ordunidif 3005  onint 3006  trsucss 3056  suc11 3093  limuni3 3123  tfi 3126  tfis 3127  limomss 3137  ordom 3141  peano5 3153  tfinds 3161  vtoclrbr 3212  opelxpex2 3279  relssres 3392  cores 3499  funss 3534  funopg 3547  imadif 3574  fneu 3592  fco 3636  rnssopab 3825  fconst5 3848  funfvima2 3853  funfvima3 3854  tfrlem1 3911  tfrlem5 3915  tfrlem11 3921  tz7.48lem 3955  tz7.48-1 3956  tz7.49 3959  tz7.49c 3960  omordi 4197  omord 4199  omass 4211  oneo 4212  oewordri 4219  oeworde 4220  omsmolem 4256  omsmo 4257  mapsn 4345  ssdomg 4408  sbthlem1 4447  fodomr 4483  pwuninel 4486  2pwuninel 4487  nneneq 4512  php 4513  infsdomnn 4532  pssnn 4534  unblem1 4540  unblem2 4541  unbnn2 4545  isfinite2OLD 4546  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  supub 4580  suplub 4581  sucprcreg 4600  inf3lem2 4614  inf3lem3 4615  infensuc 4638  noinfep 4640  trcl 4645  zfregs 4647  rankr1 4674  rankuni2 4690  hta 4728  aceq5 4740  kmlem4 4768  kmlem11 4775  kmlem12 4776  weth 4787  zorn2lem5 4792  zorn2lem6 4793  carddom 4836  sucdom 4842  ondomcard 4857  carduni 4858  alephordi 4874  cardaleph 4885  carduniima 4890  alephval2 4902  alephval3 4903  cfsuc 4915  axpowndlem3 4951  axregndlem1 4954  axregnd 4956  axacndlem1 4959  axacndlem2 4960  axacndlem3 4961  axacndlem4 4962  axacnd 4964  indpi 5034  ltrpq 5085  genpcd 5109  prlem934 5139  ltaddpr 5140  ltexprlem1 5142  ltexprlem2 5143  ltexprlem7 5148  ltaprlem 5150  ltapr 5151  prlem936 5155  reclem2pr 5157  reclem3pr 5158  reclem4pr 5159  mulcmpblnr 5183  recexsrlem 5212  mulgt0sr 5214  recexsr 5216  suppsr2 5223  pre-axsup 5291  addsubt 5384  1re 5435  recext 5684  nnleltp1t 5954  infmsup 6068  nnunb 6070  xrub 6080  primet 6195  zeot 6199  dfuz 6202  btwnz 6215  qbtwnre 6278  seq1rn2 6321  uz11t 6432  elfzlem 6473  fsequb 6523  seqzrn2 6556  creur 6742  creui 6743  cvg3 6923  facwordit 6944  fsum1 7005  fsumshftm 7032  serzcl2t 7049  2climnn 7102  2climnn0 7103  clim2serzt 7134  iserzmulc1 7136  climserzle 7147  caucvglem6 7162  isum1p 7206  isummulc1ALT 7213  fsum0diaglem2 7257  abscncflem 7274  unbenlem 7504  infxpidmlem10 7561  infxpidmlem11 7562  infmap2lem1 7579  tgss2t 7637  basgen2t 7639  bastop 7642  subbas2OLD 7645  qdensere 7751  cnconst 7780  hausnei 7784  mettri2 7813  mettri4 7814  opnin 7869  metcni 7894  metcn4i 7972  xplmi 7973  xplm 7975  xpcn 7976  iscms2lem4 7992  lmcau 7996  isgrp 8041  grpidinvlem3 8050  ringdi 8146  ringdir 8147  ringass 8148  vcdi 8171  vcdir 8172  vcass 8173  nvex 8230  nvs 8290  nvtri 8298  lnolin 8415  efifolem4 8725  hlimunii 9108  chsscm 9112  chocuni 9172  occllem6 9178  occl 9181  projlem28 9213  pjthlem12 9230  chintcl 9295  chlejb1 9399  elspansn4t 9496  osumlem4 9581  spansncv 9597  hoaddsubt 9742  lnoplt 9838  lnfnlt 9855  nmcopexlem6 9956  lnopcon 9963  nmcfnexlem6 9985  lnfncon 9990  nlelch 9994  riesz4 9996  rnbra 10040  bra11 10041  pjnormss 10096  pj3s 10135  stle 10167  stcltr2 10202  dmdmdt 10227  dmdbr5 10235  mdslmd1lem2 10253  atssmat 10305  atcvatlem 10312  irredlem1 10317  atcvat4 10324  mdsymlem2 10331  mdsymlem6 10335  sumdmdlem2 10346  dmdbr5at 10349  cdjreu 10359  ghomf1olem 10396  oooeqim2 10476  cdrci 10494  cmphmp 10521  hmeogrp 10538  top2ind 10548  fipfil2 10564  fipfil2OLD 10565  filintf 10569  iintlem1 10632  eqidob 10723  cmpassoh 10729  homgrf 10730  cmpmon 10743  idmon 10745

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

Copyright terms: Public domain