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

Theorem cmnmnd 16687
Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
cmnmnd  |-  ( G  e. CMnd  ->  G  e.  Mnd )

Proof of Theorem cmnmnd
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2443 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2443 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
31, 2iscmn 16679 . 2  |-  ( G  e. CMnd 
<->  ( G  e.  Mnd  /\ 
A. x  e.  (
Base `  G ) A. y  e.  ( Base `  G ) ( x ( +g  `  G
) y )  =  ( y ( +g  `  G ) x ) ) )
43simplbi 460 1  |-  ( G  e. CMnd  ->  G  e.  Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   A.wral 2793   ` cfv 5578  (class class class)co 6281   Basecbs 14509   +g cplusg 14574   Mndcmnd 15793  CMndccmn 16672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-cmn 16674
This theorem is referenced by:  cmn32  16690  cmn4  16691  cmn12  16692  mulgnn0di  16708  mulgmhm  16710  ghmcmn  16714  prdscmnd  16741  gsumres  16795  gsumcl2  16796  gsumf1o  16798  gsumresOLD  16799  gsumclOLD  16800  gsumf1oOLD  16801  gsumsubmcl  16804  gsumsubmclOLD  16805  gsumadd  16812  gsumaddOLD  16813  gsumsplit  16820  gsumsplitOLD  16821  gsummhm  16833  gsummhmOLD  16834  gsummulglem  16838  gsuminv  16845  gsuminvOLD  16847  gsumunsnfd  16857  gsumdifsnd  16861  gsum2d  16873  gsum2dOLD  16874  prdsgsum  16881  prdsgsumOLD  16882  srgmnd  17035  gsumvsmul  17448  gsumvsmulOLD  17449  mplcoe2OLD  18007  psrbagev1  18051  psrbagev1OLD  18052  evlslem3  18057  evlslem1  18058  ply1coeOLD  18212  frlmgsumOLD  18674  frlmgsum  18675  frlmup2  18706  islindf4  18746  mdetdiagid  18975  mdetrlin  18977  mdetrsca  18978  gsummatr01lem3  19032  gsummatr01  19034  chpscmat  19216  chp0mat  19220  chpidmat  19221  tmdgsum  20467  tmdgsum2  20468  tsms0  20516  tsmsmhm  20521  tsmsadd  20522  tgptsmscls  20525  tsmssplit  20527  tsmsxplem1  20528  tsmsxplem2  20529  imasdsf1olem  20749  lgseisenlem4  23499  xrge00  27547  xrge0omnd  27574  slmdmnd  27622  gsumle  27643  xrge0iifmhm  27794  xrge0tmdOLD  27800  esum0  27933  esumsn  27945  esumcocn  27959  gsumpr  32678  gsumdifsndf  32683
  Copyright terms: Public domain W3C validator