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

Theorem syl3an 1270
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 1181 . 2
5 syl3an.4 . 2
64, 5syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  funtpg  5643  fresaun  5761  fresaunres2  5762  ftpg  6081  eloprabga  6389  cdaenun  8575  addasspi  9294  mulasspi  9296  distrpi  9297  addcanpi  9298  mulcanpi  9299  ltapi  9302  lemul1  10419  ltdiv2  10455  zletr  10933  zdivadd  10959  nn01to3  11204  qdivcl  11232  maxle  11420  lemin  11421  maxlt  11422  ltmin  11423  xaddass  11470  xmulasslem3  11507  xadddilem  11515  iooneg  11669  fzen  11732  fzaddel  11747  fzrev  11771  fzrevral2  11793  fzshftral  11795  fzosubel2  11876  fzonn0p1p1  11894  fldiv2  11988  modmulnn  12013  modcyc2  12032  hashssdif  12475  ccatsymb  12600  ccatw2s1ass  12634  swrdccatin12lem1  12709  fsum0diag2  13598  efsub  13835  dvdsnegb  14001  muldvds1  14008  muldvds2  14009  dvdscmul  14010  dvdsmulc  14011  dvdscmulr  14012  dvdsmulcr  14013  dvds2add  14015  dvds2sub  14016  dvdstr  14018  divalglem8  14058  divalgb  14062  divalgmod  14064  ndvdsadd  14066  modgcd  14174  absmulgcd  14185  rpmulgcd  14193  hashdvds  14305  pythagtriplem1  14340  vdwlem3  14501  ressinbas  14693  gsumws2  16010  nmzsubg  16242  pmtr3ncomlem1  16498  pmtrdifellem1  16501  subcmn  16845  gexexlem  16858  lsmcom  16864  zaddablx  16876  assa2ass  17971  psrbagconf1o  18026  gsumbagdiaglem  18027  psrass1lem  18029  psrass1  18060  mplmonmul  18126  ply1opprmul  18280  coe1mul  18311  psgnghm  18616  2ndcdisj2  19958  fbssfi  20338  isfcf  20535  nmotri  21246  nghmplusg  21247  0nmhm  21262  iundisj2  21959  ovolioo  21978  uniiccdif  21987  basellem9  23362  nb3grapr  24453  hashclwwlkn  24836  rusgra0edg  24955  gxmodid  25281  issubgoi  25312  ablomul  25357  lnocoi  25672  ipasslem5  25750  hhssnv  26180  shscli  26235  shmodsi  26307  lnopmi  26919  lnopcoi  26922  cnlnadjlem2  26987  adjmul  27011  leopmul2i  27054  leoptr  27056  pjimai  27095  mdslle1i  27236  mdslle2i  27237  mdslj1i  27238  mdslj2i  27239  mdslmd1lem1  27244  mdslmd2i  27249  atexch  27300  atcvatlem  27304  chirredlem3  27311  sumdmdii  27334  sumdmdlem  27337  cdj3i  27360  iundisj2f  27449  iundisj2fi  27602  xrge0omnd  27701  binomrisefac  29164  cgr3permute3  29697  cgr3permute1  29698  cgr3com  29703  nndivsub  29922  mblfinlem2  30052  cnambfre  30063  ftc1anclem5  30094  fzmul  30233  fzadd2  30234  isismty  30297  heibor1  30306  heiborlem3  30309  elmapresaun  30704  elmapresaunres2  30705  fzneg  30920  lsmfgcl  31020  ltsubsubaddltsub  32324  nnsgrp  32505  c0snghm  32722  2zrngALT  32754  nn0sumltlt  32939  gsumpr  32950  lincsum  33030  trelded  33338  jaoded  33339  eel112  33490  el123  33561  suctrALT  33626  suctrALTcf  33722  bnj1384  34088  hlatjcl  35091  hlatjcom  35092  hlatlej1  35099  hlrelat5N  35125  2lplnmN  35283  2llnmj  35284  2lplnmj  35346
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
  Copyright terms: Public domain W3C validator