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

Theorem syl3an 1366
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  1384  euelss  3906  3elpr2eq  4426  funtpg  5930  funtpgOLD  5931  fresaun  6062  fresaunres2  6063  ftpg  6408  eloprabga  6732  cdaenun  8981  addasspi  9702  mulasspi  9704  distrpi  9705  addcanpi  9706  mulcanpi  9707  ltapi  9710  lemul1  10860  ltdiv2  10894  zletr  11406  zdivadd  11433  nn01to3  11766  qdivcl  11794  maxle  12007  lemin  12008  maxlt  12009  ltmin  12010  xaddass  12064  xmulasslem3  12101  xadddilem  12109  iooneg  12277  zltaddlt1le  12309  fzen  12343  fzaddel  12360  fzadd2  12361  fzrev  12388  fzrevral2  12410  fzshftral  12412  fzosubel2  12511  fzonn0p1p1  12530  fldiv2  12643  modmulnn  12671  modcyc2  12689  prsshashgt1  13181  hashssdif  13183  ccatsymb  13349  ccatw2s1ass  13389  swrdccatin12lem1  13465  fsum0diag2  14496  binomrisefac  14754  efsub  14811  dvdsnegb  14980  muldvds1  14987  muldvds2  14988  dvdscmul  14989  dvdsmulc  14990  dvdscmulr  14991  dvdsmulcr  14992  dvds2add  14996  dvds2sub  14997  dvdstr  14999  addmodlteqALT  15028  divalglem8  15104  divalgb  15108  divalgmod  15110  divalgmodOLD  15111  ndvdsadd  15115  modgcd  15234  absmulgcd  15247  rpmulgcd  15256  cncongr2  15363  hashdvds  15461  pythagtriplem1  15502  vdwlem3  15668  ressinbas  15917  gsumws2  17360  mulgmodid  17562  nmzsubg  17616  pmtr3ncomlem1  17874  pmtrdifellem1  17877  subcmn  18223  gexexlem  18236  lsmcom  18242  zaddablx  18256  assa2ass  19303  psrbagconf1o  19355  gsumbagdiaglem  19356  psrass1lem  19358  psrass1  19386  mplmonmul  19445  ply1opprmul  19590  coe1mul  19621  psgnghm  19907  2ndcdisj2  21241  fbssfi  21622  isfcf  21819  nmotri  22524  nghmplusg  22525  0nmhm  22540  iundisj2  23298  ovolioo  23317  uniiccdif  23327  basellem9  24796  cplgr2vpr  26310  redwlk  26550  lnocoi  27582  ipasslem5  27660  hhssabloilem  28088  hhssnv  28091  shscli  28146  shmodsi  28218  lnopmi  28829  lnopcoi  28832  cnlnadjlem2  28897  adjmul  28921  leopmul2i  28964  leoptr  28966  pjimai  29005  mdslle1i  29146  mdslle2i  29147  mdslj1i  29148  mdslj2i  29149  mdslmd1lem1  29154  mdslmd2i  29159  atexch  29210  atcvatlem  29214  chirredlem3  29221  sumdmdii  29244  sumdmdlem  29247  cdj3i  29270  iundisj2f  29375  iundisj2fi  29530  xrge0omnd  29685  bnj1384  31074  noetalem5  31841  cgr3permute3  32129  cgr3permute1  32130  cgr3com  32135  nndivsub  32431  mblfinlem2  33418  cnambfre  33429  ftc1anclem5  33460  fzmul  33508  isismty  33571  heibor1  33580  heiborlem3  33583  hlatjcl  34472  hlatjcom  34473  hlatlej1  34480  hlrelat5N  34506  2lplnmN  34664  2llnmj  34665  2lplnmj  34727  elmapresaun  37153  elmapresaunres2  37154  fzneg  37368  lsmfgcl  37463  trelded  38601  jaoded  38602  el123  38811  suctrALT  38881  suctrALTcf  38978  ltsubsubaddltsub  41078  fmtnoprmfac2lem1  41243  gboge9  41417  bgoldbtbndlem3  41460  nnsgrp  41582  c0snghm  41681  2zrngALT  41713  nn0sumltlt  41893  gsumpr  41904  lincsum  41983  dignn0fr  42160  dignn0flhalflem2  42175
  Copyright terms: Public domain W3C validator