HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 syl5.1 . 2 |- (ph -> (ps -> ch))
2 syl5.2 . . 3 |- (th -> ps)
32imim1i 16 . 2 |- ((ps -> ch) -> (th -> ch))
41, 3syl 10 1 |- (ph -> (th -> ch))
Colors of variables: wff set class
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 569  pm5.18 659  elimant 683  prlem1 769  syl3an2 859  meredith 922  ax4 970  ax5o 972  ax5 974  a4sd 983  hbnt 1000  19.21 1054  equtr2 1131  hbae 1143  dvelimfALT 1151  cbv2 1161  sbied 1193  ax11a2 1214  sb4 1221  hbsb4 1246  ax11v 1263  ax11indn 1364  ax11inda2 1368  a12study 1376  hbeu 1387  euimmo 1418  mopick 1431  moeq3 1917  sbcbid 1972  sbc19.20dv 1981  ra4sbc 1993  csbexg 2004  csbeq2d 2014  pwssun 2822  reuuni4 2882  ralxfr 2894  wereu 2940  tz7.7 2968  onfr 2981  ordtr2 2997  ordunidif 3000  onint 3001  trsucss 3051  suc11 3088  limuni3 3118  tfi 3121  tfis 3122  limomss 3132  ordom 3136  peano5 3148  tfinds 3156  vtoclrbr 3207  opelxpex2 3274  relssres 3384  cores 3491  funss 3526  funopg 3539  imadif 3566  fneu 3584  fco 3627  rnssopab 3816  fconst5 3839  funfvima2 3844  funfvima3 3845  tfrlem1 3902  tfrlem5 3906  tfrlem11 3912  tz7.48lem 3946  tz7.48-1 3947  tz7.49 3950  tz7.49c 3951  omordi 4187  omord 4189  omass 4201  oneo 4202  oewordri 4209  oeworde 4210  omsmolem 4246  omsmo 4247  mapsn 4335  ssdomg 4395  sbthlem1 4433  fodomr 4469  pwuninel 4472  2pwuninel 4473  nneneq 4498  php 4499  infsdomnn 4517  pssnn 4519  unblem1 4523  unblem2 4524  unbnn2 4528  isfinite2 4529  fiint 4540  fodomfi 4546  supub 4560  suplub 4561  sucprcreg 4580  inf3lem2 4594  inf3lem3 4595  infensuc 4618  noinfep 4620  trcl 4625  zfregs 4627  rankr1 4654  rankuni2 4670  hta 4708  aceq5 4720  kmlem4 4748  kmlem11 4755  kmlem12 4756  weth 4767  zorn2lem5 4772  zorn2lem6 4773  carddom 4816  sucdom 4822  ondomcard 4837  carduni 4838  alephordi 4854  cardaleph 4865  carduniima 4870  alephval2 4882  alephval3 4883  cfsuc 4895  axpowndlem3 4931  axregndlem1 4934  axregnd 4936  axacndlem1 4939  axacndlem2 4940  axacndlem3 4941  axacndlem4 4942  axacnd 4944  indpi 5014  ltrpq 5065  genpcd 5089  prlem934 5119  ltaddpr 5120  ltexprlem1 5122  ltexprlem2 5123  ltexprlem7 5128  ltaprlem 5130  ltapr 5131  prlem936 5135  reclem2pr 5137  reclem3pr 5138  reclem4pr 5139  mulcmpblnr 5163  recexsrlem 5192  mulgt0sr 5194  recexsr 5196  suppsr2 5203  pre-axsup 5271  addsubt 5364  1re 5415  recext 5665  nnleltp1t 5909  infmsup 6023  nnunb 6025  xrub 6035  primet 6150  zeot 6154  dfuz 6158  btwnz 6171  qbtwnre 6224  seq1rn2 6266  uz11t 6372  elfzlem 6413  fsequb 6463  seqzrn2 6496  creur 6681  creui 6682  cvg3 6868  facwordit 6889  fsum1 6951  fsumshftm 6978  serzcl2t 6995  2climnn 7047  2climnn0 7048  clim2serzt 7078  iserzmulc1 7080  climserzle 7091  caucvglem6 7106  isum1p 7149  isummulc1ALT 7156  fsum0diaglem2 7200  abscncflem 7217  unbenlem 7455  infxpidmlem10 7512  infxpidmlem11 7513  infmap2lem1 7529  tgss2t 7587  basgen2t 7589  bastop 7592  subbas2 7595  qdensere 7701  cnconst 7730  hausnei 7734  mettri2 7763  mettri4 7764  opnin 7821  metcni 7846  metcn4i 7922  xplmi 7923  xplm 7925  xpcn 7926  iscms2lem4 7942  lmcau 7946  isgrp 7991  grpidinvlem3 8000  ringdi 8098  ringdir 8099  ringass 8100  vcdi 8123  vcdir 8124  vcass 8125  nvex 8182  nvs 8242  nvtri 8250  lnolin 8362  efifolem4 8659  hlimunii 9047  chsscm 9051  chocuni 9111  occllem6 9117  occl 9120  projlem28 9152  pjthlem12 9168  chintcl 9233  chlejb1 9337  elspansn4t 9436  osumlem4 9521  spansncv 9537  hoaddsubt 9682  lnoplt 9777  lnfnlt 9794  nmcopexlem6 9894  lnopcon 9901  nmcfnexlem6 9923  lnfncon 9928  nlelch 9932  riesz4 9934  rnbra 9978  bra11 9979  pjnormss 10034  pj3s 10073  stle 10105  stcltr2 10140  dmdmdt 10165  mdslmd1lem2 10190  atssmat 10242  atcvatlem 10249  irredlem1 10254  atcvat4 10261  mdsymlem2 10268  mdsymlem6 10272  sumdmdlem2 10282  dmdbr5at 10284  cdjreu 10293  ghomf1olem 10330  oooeqim2 10407  cdrci 10417  cmphmp 10444  hmeogrp 10461  fipfil2 10475  filintf 10479  iintlem1 10512  eqidob 10603  cmpassoh 10609  homgrf 10610  cmpmon 10621  idmon 10624
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain