MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3an Structured version   Visualization version   GIF version

Theorem syl3an 1161
Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)
Hypotheses
Ref Expression
syl3an.1 (𝜑𝜓)
syl3an.2 (𝜒𝜃)
syl3an.3 (𝜏𝜂)
syl3an.4 ((𝜓𝜃𝜂) → 𝜁)
Assertion
Ref Expression
syl3an ((𝜑𝜒𝜏) → 𝜁)

Proof of Theorem syl3an
StepHypRef Expression
1 syl3an.1 . . 3 (𝜑𝜓)
2 syl3an.2 . . 3 (𝜒𝜃)
3 syl3an.3 . . 3 (𝜏𝜂)
41, 2, 33anim123i 1152 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 17 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090
This theorem is referenced by:  syl2an3an  1423  spc3egv  3563  euelss  4282  3elpr2eq  4865  funtpg  6557  fresaun  6714  fresaunres2  6715  ftpg  7103  eloprabga  7465  eloprabgaOLD  7466  elmapresaun  8819  djuenun  10107  addasspi  10832  mulasspi  10834  distrpi  10835  addcanpi  10836  mulcanpi  10837  ltapi  10840  lemul1  12008  ltdiv2  12042  zletr  12548  zdivadd  12575  eluzsub  12794  nn01to3  12867  qdivcl  12896  maxle  13111  lemin  13112  maxlt  13113  ltmin  13114  xaddass  13169  xmulasslem3  13206  xadddilem  13214  iooneg  13389  zltaddlt1le  13423  fzen  13459  fzaddel  13476  fzadd2  13477  fzrev  13505  fzrevral2  13528  fzshftral  13530  fzosubel2  13633  fzonn0p1p1  13652  fldiv2  13767  modmulnn  13795  modcyc2  13813  prsshashgt1  14311  hashssdif  14313  pfxccatin12lem4  14615  fsum0diag2  15669  binomrisefac  15926  efsub  15983  dvdsnegb  16157  muldvds1  16164  muldvds2  16165  dvdscmul  16166  dvdsmulc  16167  dvdscmulr  16168  dvdsmulcr  16169  dvds2add  16173  dvds2sub  16174  dvdstr  16177  addmodlteqALT  16208  divalglem8  16283  divalgb  16287  divalgmod  16289  ndvdsadd  16293  modgcd  16414  absmulgcd  16431  rpmulgcd  16438  cncongr2  16545  hashdvds  16648  pythagtriplem1  16689  vdwlem3  16856  ressinbas  17127  gsumws2  18653  mulgmodid  18916  nmzsubg  18968  pmtr3ncomlem1  19256  pmtrdifellem1  19259  subcmn  19616  gexexlem  19631  lsmcom  19637  zaddablx  19651  gsumpr  19733  psgnghm  20987  phlssphl  21066  assa2ass  21272  psrbagconf1o  21341  psrbagconf1oOLD  21342  gsumbagdiaglemOLD  21343  psrass1lemOLD  21345  gsumbagdiaglem  21346  psrass1lem  21348  psrass1  21377  mplmonmul  21440  ply1opprmul  21613  coe1mul  21644  2ndcdisj2  22811  fbssfi  23191  isfcf  23388  nmotri  24106  nghmplusg  24107  0nmhm  24122  iundisj2  24916  ovolioo  24935  uniiccdif  24945  basellem9  26441  cplgr2vpr  28384  redwlk  28623  clwwlknccat  29010  frgrwopreglem5a  29258  lnocoi  29702  ipasslem5  29780  hhssabloilem  30206  hhssnv  30209  shscli  30262  shmodsi  30334  lnopmi  30945  lnopcoi  30948  cnlnadjlem2  31013  adjmul  31037  leopmul2i  31080  leoptr  31082  pjimai  31121  mdslle1i  31262  mdslle2i  31263  mdslj1i  31264  mdslj2i  31265  mdslmd1lem1  31270  mdslmd2i  31275  atexch  31326  atcvatlem  31330  chirredlem3  31337  sumdmdii  31360  sumdmdlem  31363  cdj3i  31386  iundisj2f  31511  iundisj2fi  31703  xrge0omnd  31922  srafldlvec  32293  bnj1384  33647  revpfxsfxrev  33712  satffunlem2lem1  34001  cgr3permute3  34635  cgr3permute1  34636  cgr3com  34641  nndivsub  34932  lindsadd  36074  mblfinlem2  36119  cnambfre  36129  ftc1anclem5  36158  fzmul  36203  isismty  36263  heibor1  36272  heiborlem3  36275  hlatjcl  37832  hlatjcom  37833  hlatlej1  37840  hlrelat5N  37867  2lplnmN  38025  2llnmj  38026  2lplnmj  38088  factwoffsmonot  40618  isdomn4  40627  syl3an12  40630  zexpgcd  40825  dvdsexpnn  40829  elmapresaunres2  41097  fzneg  41309  lsmfgcl  41404  trelded  42854  jaoded  42855  el123  43053  suctrALT  43115  suctrALTcf  43211  fnfocofob  45318  ltsubsubaddltsub  45540  fmtnoprmfac2lem1  45765  gboge9  45963  bgoldbtbndlem3  46006  nnsgrp  46118  c0snghm  46221  2zrngALT  46253  nn0sumltlt  46433  lincsum  46517  dignn0fr  46694  dignn0flhalflem2  46709
  Copyright terms: Public domain W3C validator