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

Theorem syl3an 1310
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 1193 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
5 syl3an.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5syl 17 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  funtpg  5632  fresaun  5754  fresaunres2  5755  ftpg  6074  eloprabga  6383  cdaenun  8604  addasspi  9320  mulasspi  9322  distrpi  9323  addcanpi  9324  mulcanpi  9325  ltapi  9328  lemul1  10457  ltdiv2  10492  zletr  10981  zdivadd  11007  nn01to3  11257  qdivcl  11285  maxle  11485  lemin  11486  maxlt  11487  ltmin  11488  xaddass  11535  xmulasslem3  11572  xadddilem  11580  iooneg  11752  fzen  11816  fzaddel  11833  fzrev  11858  fzrevral2  11880  fzshftral  11882  fzosubel2  11974  fzonn0p1p1  11992  fldiv2  12088  modmulnn  12114  modcyc2  12133  hashssdif  12588  ccatsymb  12727  ccatw2s1ass  12763  swrdccatin12lem1  12840  fsum0diag2  13844  binomrisefac  14095  efsub  14154  dvdsnegb  14320  muldvds1  14327  muldvds2  14328  dvdscmul  14329  dvdsmulc  14330  dvdscmulr  14331  dvdsmulcr  14332  dvds2add  14334  dvds2sub  14335  dvdstr  14337  divalglem8  14380  divalgb  14385  divalgmod  14387  ndvdsadd  14389  modgcd  14500  absmulgcd  14515  rpmulgcd  14523  hashdvds  14723  pythagtriplem1  14766  vdwlem3  14933  ressinbas  15185  gsumws2  16626  nmzsubg  16858  pmtr3ncomlem1  17114  pmtrdifellem1  17117  subcmn  17477  gexexlem  17490  lsmcom  17496  zaddablx  17508  assa2ass  18546  psrbagconf1o  18598  gsumbagdiaglem  18599  psrass1lem  18601  psrass1  18629  mplmonmul  18688  ply1opprmul  18832  coe1mul  18863  psgnghm  19148  2ndcdisj2  20472  fbssfi  20852  isfcf  21049  nmotri  21760  nghmplusg  21761  0nmhm  21776  iundisj2  22502  ovolioo  22521  uniiccdif  22535  basellem9  24015  nb3grapr  25181  hashclwwlkn  25564  rusgra0edg  25683  gxmodid  26007  issubgoi  26038  ablomul  26083  lnocoi  26398  ipasslem5  26476  hhssnv  26915  shscli  26970  shmodsi  27042  lnopmi  27653  lnopcoi  27656  cnlnadjlem2  27721  adjmul  27745  leopmul2i  27788  leoptr  27790  pjimai  27829  mdslle1i  27970  mdslle2i  27971  mdslj1i  27972  mdslj2i  27973  mdslmd1lem1  27978  mdslmd2i  27983  atexch  28034  atcvatlem  28038  chirredlem3  28045  sumdmdii  28068  sumdmdlem  28071  cdj3i  28094  iundisj2f  28200  iundisj2fi  28373  xrge0omnd  28474  bnj1384  29841  cgr3permute3  30814  cgr3permute1  30815  cgr3com  30820  nndivsub  31117  mblfinlem2  31978  cnambfre  31989  ftc1anclem5  32021  fzmul  32069  fzadd2  32070  isismty  32133  heibor1  32142  heiborlem3  32145  hlatjcl  32932  hlatjcom  32933  hlatlej1  32940  hlrelat5N  32966  2lplnmN  33124  2llnmj  33125  2lplnmj  33187  elmapresaun  35613  elmapresaunres2  35614  fzneg  35832  lsmfgcl  35932  trelded  36932  jaoded  36933  eel112  37083  el123  37151  suctrALT  37222  suctrALTcf  37319  gboage9  38865  bgoldbtbndlem3  38902  ltsubsubaddltsub  39048  cplgr2vpr  39500  nnsgrp  39870  c0snghm  39969  2zrngALT  40001  nn0sumltlt  40184  gsumpr  40195  lincsum  40275  dignn0fr  40465  dignn0flhalflem2  40480
  Copyright terms: Public domain W3C validator