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

Theorem syl3an 1408
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 1266 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 17 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  syl2an3an  1426  euelss  3947  3elpr2eq  4467  funtpg  5980  funtpgOLD  5981  fresaun  6113  fresaunres2  6114  ftpg  6463  eloprabga  6789  cdaenun  9034  addasspi  9755  mulasspi  9757  distrpi  9758  addcanpi  9759  mulcanpi  9760  ltapi  9763  lemul1  10913  ltdiv2  10947  zletr  11459  zdivadd  11486  nn01to3  11819  qdivcl  11847  maxle  12060  lemin  12061  maxlt  12062  ltmin  12063  xaddass  12117  xmulasslem3  12154  xadddilem  12162  iooneg  12330  zltaddlt1le  12362  fzen  12396  fzaddel  12413  fzadd2  12414  fzrev  12441  fzrevral2  12464  fzshftral  12466  fzosubel2  12567  fzonn0p1p1  12586  fldiv2  12700  modmulnn  12728  modcyc2  12746  prsshashgt1  13236  hashssdif  13238  ccatsymb  13400  ccatw2s1ass  13451  swrdccatin12lem1  13530  fsum0diag2  14559  binomrisefac  14817  efsub  14874  dvdsnegb  15046  muldvds1  15053  muldvds2  15054  dvdscmul  15055  dvdsmulc  15056  dvdscmulr  15057  dvdsmulcr  15058  dvds2add  15062  dvds2sub  15063  dvdstr  15065  addmodlteqALT  15094  divalglem8  15170  divalgb  15174  divalgmod  15176  divalgmodOLD  15177  ndvdsadd  15181  modgcd  15300  absmulgcd  15313  rpmulgcd  15322  cncongr2  15429  hashdvds  15527  pythagtriplem1  15568  vdwlem3  15734  ressinbas  15983  gsumws2  17426  mulgmodid  17628  nmzsubg  17682  pmtr3ncomlem1  17939  pmtrdifellem1  17942  subcmn  18288  gexexlem  18301  lsmcom  18307  zaddablx  18321  assa2ass  19370  psrbagconf1o  19422  gsumbagdiaglem  19423  psrass1lem  19425  psrass1  19453  mplmonmul  19512  ply1opprmul  19657  coe1mul  19688  psgnghm  19974  2ndcdisj2  21308  fbssfi  21688  isfcf  21885  nmotri  22590  nghmplusg  22591  0nmhm  22606  iundisj2  23363  ovolioo  23382  uniiccdif  23392  basellem9  24860  cplgr2vpr  26385  redwlk  26625  frgrwopreglem5a  27291  2clwwlk2clwwlklem1  27327  clwwlknccat  27333  lnocoi  27740  ipasslem5  27818  hhssabloilem  28246  hhssnv  28249  shscli  28304  shmodsi  28376  lnopmi  28987  lnopcoi  28990  cnlnadjlem2  29055  adjmul  29079  leopmul2i  29122  leoptr  29124  pjimai  29163  mdslle1i  29304  mdslle2i  29305  mdslj1i  29306  mdslj2i  29307  mdslmd1lem1  29312  mdslmd2i  29317  atexch  29368  atcvatlem  29372  chirredlem3  29379  sumdmdii  29402  sumdmdlem  29405  cdj3i  29428  iundisj2f  29529  iundisj2fi  29684  xrge0omnd  29839  bnj1384  31226  noetalem5  31992  cgr3permute3  32279  cgr3permute1  32280  cgr3com  32285  nndivsub  32581  mblfinlem2  33577  cnambfre  33588  ftc1anclem5  33619  fzmul  33667  isismty  33730  heibor1  33739  heiborlem3  33742  hlatjcl  34971  hlatjcom  34972  hlatlej1  34979  hlrelat5N  35005  2lplnmN  35163  2llnmj  35164  2lplnmj  35226  elmapresaun  37651  elmapresaunres2  37652  fzneg  37866  lsmfgcl  37961  trelded  39098  jaoded  39099  el123  39308  suctrALT  39375  suctrALTcf  39472  ltsubsubaddltsub  41640  fmtnoprmfac2lem1  41803  gboge9  41977  bgoldbtbndlem3  42020  nnsgrp  42142  c0snghm  42241  2zrngALT  42273  nn0sumltlt  42453  gsumpr  42464  lincsum  42543  dignn0fr  42720  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator