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

Theorem syl3an 1307
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 1191 . 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 983
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 985
This theorem is referenced by:  funtpg  5649  fresaun  5769  fresaunres2  5770  ftpg  6087  eloprabga  6395  cdaenun  8606  addasspi  9322  mulasspi  9324  distrpi  9325  addcanpi  9326  mulcanpi  9327  ltapi  9330  lemul1  10459  ltdiv2  10494  zletr  10983  zdivadd  11009  nn01to3  11259  qdivcl  11287  maxle  11487  lemin  11488  maxlt  11489  ltmin  11490  xaddass  11537  xmulasslem3  11574  xadddilem  11582  iooneg  11754  fzen  11818  fzaddel  11835  fzrev  11860  fzrevral2  11882  fzshftral  11884  fzosubel2  11975  fzonn0p1p1  11993  fldiv2  12089  modmulnn  12115  modcyc2  12134  hashssdif  12588  ccatsymb  12725  ccatw2s1ass  12759  swrdccatin12lem1  12836  fsum0diag2  13837  binomrisefac  14088  efsub  14147  dvdsnegb  14313  muldvds1  14320  muldvds2  14321  dvdscmul  14322  dvdsmulc  14323  dvdscmulr  14324  dvdsmulcr  14325  dvds2add  14327  dvds2sub  14328  dvdstr  14330  divalglem8  14373  divalgb  14378  divalgmod  14380  ndvdsadd  14382  modgcd  14493  absmulgcd  14508  rpmulgcd  14516  hashdvds  14716  pythagtriplem1  14759  vdwlem3  14926  ressinbas  15178  gsumws2  16619  nmzsubg  16851  pmtr3ncomlem1  17107  pmtrdifellem1  17110  subcmn  17470  gexexlem  17483  lsmcom  17489  zaddablx  17501  assa2ass  18539  psrbagconf1o  18591  gsumbagdiaglem  18592  psrass1lem  18594  psrass1  18622  mplmonmul  18681  ply1opprmul  18825  coe1mul  18856  psgnghm  19140  2ndcdisj2  20464  fbssfi  20844  isfcf  21041  nmotri  21752  nghmplusg  21753  0nmhm  21768  iundisj2  22494  ovolioo  22513  uniiccdif  22527  basellem9  24007  nb3grapr  25173  hashclwwlkn  25556  rusgra0edg  25675  gxmodid  25999  issubgoi  26030  ablomul  26075  lnocoi  26390  ipasslem5  26468  hhssnv  26907  shscli  26962  shmodsi  27034  lnopmi  27645  lnopcoi  27648  cnlnadjlem2  27713  adjmul  27737  leopmul2i  27780  leoptr  27782  pjimai  27821  mdslle1i  27962  mdslle2i  27963  mdslj1i  27964  mdslj2i  27965  mdslmd1lem1  27970  mdslmd2i  27975  atexch  28026  atcvatlem  28030  chirredlem3  28037  sumdmdii  28060  sumdmdlem  28063  cdj3i  28086  iundisj2f  28196  iundisj2fi  28373  xrge0omnd  28475  bnj1384  29843  cgr3permute3  30813  cgr3permute1  30814  cgr3com  30819  nndivsub  31116  mblfinlem2  31898  cnambfre  31909  ftc1anclem5  31941  fzmul  31989  fzadd2  31990  isismty  32053  heibor1  32062  heiborlem3  32065  hlatjcl  32857  hlatjcom  32858  hlatlej1  32865  hlrelat5N  32891  2lplnmN  33049  2llnmj  33050  2lplnmj  33112  elmapresaun  35538  elmapresaunres2  35539  fzneg  35758  lsmfgcl  35858  trelded  36796  jaoded  36797  eel112  36948  el123  37018  suctrALT  37089  suctrALTcf  37186  gboage9  38583  bgoldbtbndlem3  38620  ltsubsubaddltsub  38743  nnsgrp  39121  c0snghm  39220  2zrngALT  39252  nn0sumltlt  39437  gsumpr  39448  lincsum  39528  dignn0fr  39718  dignn0flhalflem2  39733
  Copyright terms: Public domain W3C validator