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

Theorem syl3an 1152
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 1143 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 17 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  syl2an3an  1414  spc3egv  3601  euelss  4287  3elpr2eq  4829  funtpg  6402  fresaun  6542  fresaunres2  6543  ftpg  6910  eloprabga  7250  elmapresaun  8433  djuenun  9584  addasspi  10305  mulasspi  10307  distrpi  10308  addcanpi  10309  mulcanpi  10310  ltapi  10313  lemul1  11480  ltdiv2  11514  zletr  12014  zdivadd  12041  nn01to3  12329  qdivcl  12357  maxle  12572  lemin  12573  maxlt  12574  ltmin  12575  xaddass  12630  xmulasslem3  12667  xadddilem  12675  iooneg  12845  zltaddlt1le  12878  fzen  12912  fzaddel  12929  fzadd2  12930  fzrev  12958  fzrevral2  12981  fzshftral  12983  fzosubel2  13085  fzonn0p1p1  13104  fldiv2  13217  modmulnn  13245  modcyc2  13263  prsshashgt1  13759  hashssdif  13761  ccatw2s1assOLD  13978  pfxccatin12lem4  14076  fsum0diag2  15126  binomrisefac  15384  efsub  15441  dvdsnegb  15615  muldvds1  15622  muldvds2  15623  dvdscmul  15624  dvdsmulc  15625  dvdscmulr  15626  dvdsmulcr  15627  dvds2add  15631  dvds2sub  15632  dvdstr  15634  addmodlteqALT  15663  divalglem8  15739  divalgb  15743  divalgmod  15745  ndvdsadd  15749  modgcd  15868  absmulgcd  15885  rpmulgcd  15894  cncongr2  16000  hashdvds  16100  pythagtriplem1  16141  vdwlem3  16307  ressinbas  16548  gsumws2  17995  mulgmodid  18204  nmzsubg  18255  pmtr3ncomlem1  18530  pmtrdifellem1  18533  subcmn  18886  gexexlem  18901  lsmcom  18907  zaddablx  18921  gsumpr  19004  assa2ass  20023  psrbagconf1o  20082  gsumbagdiaglem  20083  psrass1lem  20085  psrass1  20113  mplmonmul  20173  ply1opprmul  20335  coe1mul  20366  psgnghm  20652  phlssphl  20731  2ndcdisj2  21993  fbssfi  22373  isfcf  22570  nmotri  23275  nghmplusg  23276  0nmhm  23291  iundisj2  24077  ovolioo  24096  uniiccdif  24106  basellem9  25593  cplgr2vpr  27142  redwlk  27381  clwwlknccat  27769  frgrwopreglem5a  28017  lnocoi  28461  ipasslem5  28539  hhssabloilem  28965  hhssnv  28968  shscli  29021  shmodsi  29093  lnopmi  29704  lnopcoi  29707  cnlnadjlem2  29772  adjmul  29796  leopmul2i  29839  leoptr  29841  pjimai  29880  mdslle1i  30021  mdslle2i  30022  mdslj1i  30023  mdslj2i  30024  mdslmd1lem1  30029  mdslmd2i  30034  atexch  30085  atcvatlem  30089  chirredlem3  30096  sumdmdii  30119  sumdmdlem  30122  cdj3i  30145  iundisj2f  30268  iundisj2fi  30446  xrge0omnd  30639  srafldlvec  30890  bnj1384  32201  revpfxsfxrev  32259  satffunlem2lem1  32548  noetalem5  33118  cgr3permute3  33405  cgr3permute1  33406  cgr3com  33411  nndivsub  33702  lindsadd  34766  mblfinlem2  34811  cnambfre  34821  ftc1anclem5  34852  fzmul  34897  isismty  34960  heibor1  34969  heiborlem3  34972  hlatjcl  36383  hlatjcom  36384  hlatlej1  36391  hlrelat5N  36417  2lplnmN  36575  2llnmj  36576  2lplnmj  36638  zexpgcd  39063  elmapresaunres2  39246  fzneg  39457  lsmfgcl  39552  trelded  40776  jaoded  40777  el123  40975  suctrALT  41037  suctrALTcf  41133  ltsubsubaddltsub  43378  fmtnoprmfac2lem1  43605  gboge9  43806  bgoldbtbndlem3  43849  nnsgrp  43961  c0snghm  44115  2zrngALT  44147  nn0sumltlt  44326  lincsum  44412  dignn0fr  44589  dignn0flhalflem2  44604
  Copyright terms: Public domain W3C validator