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

Theorem syl3an 1272
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 1182 . 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 974
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 369  df-3an 976
This theorem is referenced by:  funtpg  5575  fresaun  5695  fresaunres2  5696  ftpg  6017  eloprabga  6326  cdaenun  8506  addasspi  9223  mulasspi  9225  distrpi  9226  addcanpi  9227  mulcanpi  9228  ltapi  9231  lemul1  10355  ltdiv2  10390  zletr  10869  zdivadd  10895  nn01to3  11138  qdivcl  11166  maxle  11362  lemin  11363  maxlt  11364  ltmin  11365  xaddass  11412  xmulasslem3  11449  xadddilem  11457  iooneg  11611  fzen  11674  fzaddel  11690  fzrev  11714  fzrevral2  11736  fzshftral  11738  fzosubel2  11825  fzonn0p1p1  11843  fldiv2  11939  modmulnn  11965  modcyc2  11984  hashssdif  12431  ccatsymb  12561  ccatw2s1ass  12595  swrdccatin12lem1  12672  fsum0diag2  13656  binomrisefac  13894  efsub  13936  dvdsnegb  14102  muldvds1  14109  muldvds2  14110  dvdscmul  14111  dvdsmulc  14112  dvdscmulr  14113  dvdsmulcr  14114  dvds2add  14116  dvds2sub  14117  dvdstr  14119  divalglem8  14159  divalgb  14163  divalgmod  14165  ndvdsadd  14167  modgcd  14275  absmulgcd  14286  rpmulgcd  14294  hashdvds  14406  pythagtriplem1  14441  vdwlem3  14602  ressinbas  14796  gsumws2  16226  nmzsubg  16458  pmtr3ncomlem1  16714  pmtrdifellem1  16717  subcmn  17061  gexexlem  17074  lsmcom  17080  zaddablx  17092  assa2ass  18183  psrbagconf1o  18238  gsumbagdiaglem  18239  psrass1lem  18241  psrass1  18272  mplmonmul  18338  ply1opprmul  18492  coe1mul  18523  psgnghm  18806  2ndcdisj2  20142  fbssfi  20522  isfcf  20719  nmotri  21430  nghmplusg  21431  0nmhm  21446  iundisj2  22143  ovolioo  22162  uniiccdif  22171  basellem9  23635  nb3grapr  24751  hashclwwlkn  25134  rusgra0edg  25253  gxmodid  25575  issubgoi  25606  ablomul  25651  lnocoi  25966  ipasslem5  26044  hhssnv  26474  shscli  26529  shmodsi  26601  lnopmi  27212  lnopcoi  27215  cnlnadjlem2  27280  adjmul  27304  leopmul2i  27347  leoptr  27349  pjimai  27388  mdslle1i  27529  mdslle2i  27530  mdslj1i  27531  mdslj2i  27532  mdslmd1lem1  27537  mdslmd2i  27542  atexch  27593  atcvatlem  27597  chirredlem3  27604  sumdmdii  27627  sumdmdlem  27630  cdj3i  27653  iundisj2f  27762  iundisj2fi  27930  xrge0omnd  28033  bnj1384  29296  cgr3permute3  30358  cgr3permute1  30359  cgr3com  30364  nndivsub  30677  mblfinlem2  31405  cnambfre  31416  ftc1anclem5  31448  fzmul  31496  fzadd2  31497  isismty  31560  heibor1  31569  heiborlem3  31572  hlatjcl  32365  hlatjcom  32366  hlatlej1  32373  hlrelat5N  32399  2lplnmN  32557  2llnmj  32558  2lplnmj  32620  elmapresaun  35046  elmapresaunres2  35047  fzneg  35262  lsmfgcl  35363  trelded  36343  jaoded  36344  eel112  36495  el123  36566  suctrALT  36637  suctrALTcf  36734  gboage9  37798  bgoldbtbndlem3  37835  ltsubsubaddltsub  37936  nnsgrp  38114  c0snghm  38213  2zrngALT  38245  nn0sumltlt  38430  gsumpr  38441  lincsum  38521  dignn0fr  38712  dignn0flhalflem2  38727
  Copyright terms: Public domain W3C validator