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

Theorem syl3an 1163
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 1154 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 17 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  syl2an3an  1532  euelss  4062  3elpr2eq  4573  funtpg  6084  fresaun  6215  fresaunres2  6216  ftpg  6566  eloprabga  6894  cdaenun  9198  addasspi  9919  mulasspi  9921  distrpi  9922  addcanpi  9923  mulcanpi  9924  ltapi  9927  lemul1  11077  ltdiv2  11111  zletr  11623  zdivadd  11650  nn01to3  11984  qdivcl  12012  maxle  12227  lemin  12228  maxlt  12229  ltmin  12230  xaddass  12284  xmulasslem3  12321  xadddilem  12329  iooneg  12499  zltaddlt1le  12531  fzen  12565  fzaddel  12582  fzadd2  12583  fzrev  12610  fzrevral2  12633  fzshftral  12635  fzosubel2  12736  fzonn0p1p1  12755  fldiv2  12868  modmulnn  12896  modcyc2  12914  prsshashgt1  13400  hashssdif  13402  ccatsymb  13564  ccatw2s1ass  13614  swrdccatin12lem1  13693  fsum0diag2  14722  binomrisefac  14979  efsub  15036  dvdsnegb  15208  muldvds1  15215  muldvds2  15216  dvdscmul  15217  dvdsmulc  15218  dvdscmulr  15219  dvdsmulcr  15220  dvds2add  15224  dvds2sub  15225  dvdstr  15227  addmodlteqALT  15256  divalglem8  15331  divalgb  15335  divalgmod  15337  divalgmodOLD  15338  ndvdsadd  15342  modgcd  15461  absmulgcd  15474  rpmulgcd  15483  cncongr2  15589  hashdvds  15687  pythagtriplem1  15728  vdwlem3  15894  ressinbas  16143  gsumws2  17587  mulgmodid  17789  nmzsubg  17843  pmtr3ncomlem1  18100  pmtrdifellem1  18103  subcmn  18449  gexexlem  18462  lsmcom  18468  zaddablx  18482  assa2ass  19537  psrbagconf1o  19589  gsumbagdiaglem  19590  psrass1lem  19592  psrass1  19620  mplmonmul  19679  ply1opprmul  19824  coe1mul  19855  psgnghm  20141  2ndcdisj2  21481  fbssfi  21861  isfcf  22058  nmotri  22763  nghmplusg  22764  0nmhm  22779  iundisj2  23537  ovolioo  23556  uniiccdif  23566  basellem9  25036  cplgr2vpr  26564  redwlk  26804  clwwlknccat  27221  frgrwopreglem5a  27493  lnocoi  27952  ipasslem5  28030  hhssabloilem  28458  hhssnv  28461  shscli  28516  shmodsi  28588  lnopmi  29199  lnopcoi  29202  cnlnadjlem2  29267  adjmul  29291  leopmul2i  29334  leoptr  29336  pjimai  29375  mdslle1i  29516  mdslle2i  29517  mdslj1i  29518  mdslj2i  29519  mdslmd1lem1  29524  mdslmd2i  29529  atexch  29580  atcvatlem  29584  chirredlem3  29591  sumdmdii  29614  sumdmdlem  29617  cdj3i  29640  iundisj2f  29741  iundisj2fi  29896  xrge0omnd  30051  bnj1384  31438  noetalem5  32204  cgr3permute3  32491  cgr3permute1  32492  cgr3com  32497  nndivsub  32793  mblfinlem2  33780  cnambfre  33790  ftc1anclem5  33821  fzmul  33869  isismty  33932  heibor1  33941  heiborlem3  33944  hlatjcl  35175  hlatjcom  35176  hlatlej1  35183  hlrelat5N  35209  2lplnmN  35367  2llnmj  35368  2lplnmj  35430  elmapresaun  37860  elmapresaunres2  37861  fzneg  38075  lsmfgcl  38170  trelded  39306  jaoded  39307  el123  39516  suctrALT  39583  suctrALTcf  39680  ltsubsubaddltsub  41843  fmtnoprmfac2lem1  42006  gboge9  42180  bgoldbtbndlem3  42223  nnsgrp  42345  c0snghm  42444  2zrngALT  42476  nn0sumltlt  42656  gsumpr  42667  lincsum  42746  dignn0fr  42923  dignn0flhalflem2  42938
  Copyright terms: Public domain W3C validator