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

Theorem syl3an 1365
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 1245 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 17 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  syl2an3an  1383  euelss  3890  funtpg  5900  funtpgOLD  5901  fresaun  6032  fresaunres2  6033  ftpg  6377  eloprabga  6700  cdaenun  8940  addasspi  9661  mulasspi  9663  distrpi  9664  addcanpi  9665  mulcanpi  9666  ltapi  9669  lemul1  10819  ltdiv2  10853  zletr  11365  zdivadd  11392  nn01to3  11725  qdivcl  11753  maxle  11965  lemin  11966  maxlt  11967  ltmin  11968  xaddass  12022  xmulasslem3  12059  xadddilem  12067  iooneg  12234  zltaddlt1le  12266  fzen  12300  fzaddel  12317  fzadd2  12318  fzrev  12345  fzrevral2  12367  fzshftral  12369  fzosubel2  12468  fzonn0p1p1  12487  fldiv2  12600  modmulnn  12628  modcyc2  12646  prsshashgt1  13138  hashssdif  13140  ccatsymb  13305  ccatw2s1ass  13345  swrdccatin12lem1  13421  fsum0diag2  14443  binomrisefac  14698  efsub  14755  dvdsnegb  14923  muldvds1  14930  muldvds2  14931  dvdscmul  14932  dvdsmulc  14933  dvdscmulr  14934  dvdsmulcr  14935  dvds2add  14939  dvds2sub  14940  dvdstr  14942  addmodlteqALT  14971  divalglem8  15047  divalgb  15051  divalgmod  15053  divalgmodOLD  15054  ndvdsadd  15058  modgcd  15177  absmulgcd  15190  rpmulgcd  15199  cncongr2  15306  hashdvds  15404  pythagtriplem1  15445  vdwlem3  15611  ressinbas  15857  gsumws2  17300  mulgmodid  17502  nmzsubg  17556  pmtr3ncomlem1  17814  pmtrdifellem1  17817  subcmn  18163  gexexlem  18176  lsmcom  18182  zaddablx  18196  assa2ass  19241  psrbagconf1o  19293  gsumbagdiaglem  19294  psrass1lem  19296  psrass1  19324  mplmonmul  19383  ply1opprmul  19528  coe1mul  19559  psgnghm  19845  2ndcdisj2  21170  fbssfi  21551  isfcf  21748  nmotri  22453  nghmplusg  22454  0nmhm  22469  iundisj2  23224  ovolioo  23243  uniiccdif  23252  basellem9  24715  cplgr2vpr  26216  redwlk  26438  lnocoi  27458  ipasslem5  27536  hhssabloilem  27964  hhssnv  27967  shscli  28022  shmodsi  28094  lnopmi  28705  lnopcoi  28708  cnlnadjlem2  28773  adjmul  28797  leopmul2i  28840  leoptr  28842  pjimai  28881  mdslle1i  29022  mdslle2i  29023  mdslj1i  29024  mdslj2i  29025  mdslmd1lem1  29030  mdslmd2i  29035  atexch  29086  atcvatlem  29090  chirredlem3  29097  sumdmdii  29120  sumdmdlem  29123  cdj3i  29146  iundisj2f  29245  iundisj2fi  29394  xrge0omnd  29493  bnj1384  30805  cgr3permute3  31793  cgr3permute1  31794  cgr3com  31799  nndivsub  32095  mblfinlem2  33076  cnambfre  33087  ftc1anclem5  33118  fzmul  33166  isismty  33229  heibor1  33238  heiborlem3  33241  hlatjcl  34130  hlatjcom  34131  hlatlej1  34138  hlrelat5N  34164  2lplnmN  34322  2llnmj  34323  2lplnmj  34385  elmapresaun  36811  elmapresaunres2  36812  fzneg  37026  lsmfgcl  37121  trelded  38260  jaoded  38261  el123  38470  suctrALT  38541  suctrALTcf  38638  ltsubsubaddltsub  40609  fmtnoprmfac2lem1  40774  gboage9  40944  bgoldbtbndlem3  40981  nnsgrp  41102  c0snghm  41201  2zrngALT  41233  nn0sumltlt  41413  gsumpr  41424  lincsum  41503  dignn0fr  41684  dignn0flhalflem2  41699
  Copyright terms: Public domain W3C validator