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

Theorem syl3an 1270
Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)
Hypotheses
Ref Expression
syl3an.1  |-  ( ph  ->  ps )
syl3an.2  |-  ( ch 
->  th )
syl3an.3  |-  ( ta 
->  et )
syl3an.4  |-  ( ( ps  /\  th  /\  et )  ->  ze )
Assertion
Ref Expression
syl3an  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )

Proof of Theorem syl3an
StepHypRef Expression
1 syl3an.1 . . 3  |-  ( ph  ->  ps )
2 syl3an.2 . . 3  |-  ( ch 
->  th )
3 syl3an.3 . . 3  |-  ( ta 
->  et )
41, 2, 33anim123i 1181 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
5 syl3an.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5syl 16 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  funtpg  5644  fresaun  5762  fresaunres2  5763  ftpg  6082  eloprabga  6388  cdaenun  8571  addasspi  9290  mulasspi  9292  distrpi  9293  addcanpi  9294  mulcanpi  9295  ltapi  9298  lemul1  10415  ltdiv2  10450  zletr  10929  zdivadd  10955  nn01to3  11200  qdivcl  11228  maxle  11416  lemin  11417  maxlt  11418  ltmin  11419  xaddass  11466  xmulasslem3  11503  xadddilem  11511  iooneg  11665  fzen  11728  fzaddel  11743  fzrev  11767  fzrevral2  11789  fzshftral  11791  fzosubel2  11878  fzonn0p1p1  11896  fldiv2  11990  modmulnn  12015  modcyc2  12034  hashssdif  12478  ccatsymb  12608  ccatw2s1ass  12642  swrdccatin12lem1  12720  fsum0diag2  13609  efsub  13846  dvdsnegb  14012  muldvds1  14019  muldvds2  14020  dvdscmul  14021  dvdsmulc  14022  dvdscmulr  14023  dvdsmulcr  14024  dvds2add  14026  dvds2sub  14027  dvdstr  14029  divalglem8  14069  divalgb  14073  divalgmod  14075  ndvdsadd  14077  modgcd  14185  absmulgcd  14196  rpmulgcd  14204  hashdvds  14316  pythagtriplem1  14351  vdwlem3  14512  ressinbas  14706  gsumws2  16136  nmzsubg  16368  pmtr3ncomlem1  16624  pmtrdifellem1  16627  subcmn  16971  gexexlem  16984  lsmcom  16990  zaddablx  17002  assa2ass  18097  psrbagconf1o  18152  gsumbagdiaglem  18153  psrass1lem  18155  psrass1  18186  mplmonmul  18252  ply1opprmul  18406  coe1mul  18437  psgnghm  18742  2ndcdisj2  20083  fbssfi  20463  isfcf  20660  nmotri  21371  nghmplusg  21372  0nmhm  21387  iundisj2  22084  ovolioo  22103  uniiccdif  22112  basellem9  23487  nb3grapr  24579  hashclwwlkn  24962  rusgra0edg  25081  gxmodid  25407  issubgoi  25438  ablomul  25483  lnocoi  25798  ipasslem5  25876  hhssnv  26306  shscli  26361  shmodsi  26433  lnopmi  27045  lnopcoi  27048  cnlnadjlem2  27113  adjmul  27137  leopmul2i  27180  leoptr  27182  pjimai  27221  mdslle1i  27362  mdslle2i  27363  mdslj1i  27364  mdslj2i  27365  mdslmd1lem1  27370  mdslmd2i  27375  atexch  27426  atcvatlem  27430  chirredlem3  27437  sumdmdii  27460  sumdmdlem  27463  cdj3i  27486  iundisj2f  27586  iundisj2fi  27754  xrge0omnd  27853  binomrisefac  29339  cgr3permute3  29859  cgr3permute1  29860  cgr3com  29865  nndivsub  30084  mblfinlem2  30214  cnambfre  30225  ftc1anclem5  30256  fzmul  30395  fzadd2  30396  isismty  30459  heibor1  30468  heiborlem3  30471  elmapresaun  30866  elmapresaunres2  30867  fzneg  31082  lsmfgcl  31182  ltsubsubaddltsub  32546  nnsgrp  32725  c0snghm  32824  2zrngALT  32856  nn0sumltlt  33041  gsumpr  33052  lincsum  33132  trelded  33439  jaoded  33440  eel112  33591  el123  33662  suctrALT  33727  suctrALTcf  33823  bnj1384  34189  hlatjcl  35192  hlatjcom  35193  hlatlej1  35200  hlrelat5N  35226  2lplnmN  35384  2llnmj  35385  2lplnmj  35447
  Copyright terms: Public domain W3C validator