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

Theorem syl3an 1360
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 1240 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 17 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  syl2an3an  1378  euelss  3873  funtpg  5856  funtpgOLD  5857  fresaun  5988  fresaunres2  5989  ftpg  6328  eloprabga  6645  cdaenun  8879  addasspi  9596  mulasspi  9598  distrpi  9599  addcanpi  9600  mulcanpi  9601  ltapi  9604  lemul1  10754  ltdiv2  10788  zletr  11298  zdivadd  11324  nn01to3  11657  qdivcl  11685  maxle  11896  lemin  11897  maxlt  11898  ltmin  11899  xaddass  11951  xmulasslem3  11988  xadddilem  11996  iooneg  12163  zltaddlt1le  12195  fzen  12229  fzaddel  12246  fzadd2  12247  fzrev  12273  fzrevral2  12295  fzshftral  12297  fzosubel2  12395  fzonn0p1p1  12413  fldiv2  12522  modmulnn  12550  modcyc2  12568  prsshashgt1  13059  hashssdif  13061  ccatsymb  13219  ccatw2s1ass  13259  swrdccatin12lem1  13335  fsum0diag2  14357  binomrisefac  14612  efsub  14669  dvdsnegb  14837  muldvds1  14844  muldvds2  14845  dvdscmul  14846  dvdsmulc  14847  dvdscmulr  14848  dvdsmulcr  14849  dvds2add  14853  dvds2sub  14854  dvdstr  14856  addmodlteqALT  14885  divalglem8  14961  divalgb  14965  divalgmod  14967  divalgmodOLD  14968  ndvdsadd  14972  modgcd  15091  absmulgcd  15104  rpmulgcd  15113  cncongr2  15220  hashdvds  15318  pythagtriplem1  15359  vdwlem3  15525  ressinbas  15763  gsumws2  17202  mulgmodid  17404  nmzsubg  17458  pmtr3ncomlem1  17716  pmtrdifellem1  17719  subcmn  18065  gexexlem  18078  lsmcom  18084  zaddablx  18098  assa2ass  19143  psrbagconf1o  19195  gsumbagdiaglem  19196  psrass1lem  19198  psrass1  19226  mplmonmul  19285  ply1opprmul  19430  coe1mul  19461  psgnghm  19745  2ndcdisj2  21070  fbssfi  21451  isfcf  21648  nmotri  22353  nghmplusg  22354  0nmhm  22369  iundisj2  23124  ovolioo  23143  uniiccdif  23152  basellem9  24615  nb3grapr  25982  hashclwwlkn  26363  rusgra0edg  26482  lnocoi  26996  ipasslem5  27074  hhssabloilem  27502  hhssnv  27505  shscli  27560  shmodsi  27632  lnopmi  28243  lnopcoi  28246  cnlnadjlem2  28311  adjmul  28335  leopmul2i  28378  leoptr  28380  pjimai  28419  mdslle1i  28560  mdslle2i  28561  mdslj1i  28562  mdslj2i  28563  mdslmd1lem1  28568  mdslmd2i  28573  atexch  28624  atcvatlem  28628  chirredlem3  28635  sumdmdii  28658  sumdmdlem  28661  cdj3i  28684  iundisj2f  28785  iundisj2fi  28943  xrge0omnd  29042  bnj1384  30354  cgr3permute3  31324  cgr3permute1  31325  cgr3com  31330  nndivsub  31626  mblfinlem2  32617  cnambfre  32628  ftc1anclem5  32659  fzmul  32707  isismty  32770  heibor1  32779  heiborlem3  32782  hlatjcl  33671  hlatjcom  33672  hlatlej1  33679  hlrelat5N  33705  2lplnmN  33863  2llnmj  33864  2lplnmj  33926  elmapresaun  36352  elmapresaunres2  36353  fzneg  36567  lsmfgcl  36662  trelded  37802  jaoded  37803  el123  38012  suctrALT  38083  suctrALTcf  38180  fmtnoprmfac2lem1  40016  gboage9  40186  bgoldbtbndlem3  40223  ltsubsubaddltsub  40347  cplgr2vpr  40655  red1wlk  40881  nnsgrp  41607  c0snghm  41706  2zrngALT  41738  nn0sumltlt  41921  gsumpr  41932  lincsum  42012  dignn0fr  42193  dignn0flhalflem2  42208
  Copyright terms: Public domain W3C validator