Theorem cmnmnd 19763

Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)

Assertion

Ref	Expression
cmnmnd	⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Proof of Theorem cmnmnd

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2737	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2737	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3	1, 2	iscmn 19755	. 2 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))
4	3	simplbi 496	1 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  Mndcmnd 18693  CMndccmn 19746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-cmn 19748

This theorem is referenced by:  cmn32  19766  cmn4  19767  cmn12  19768  cmnmndd  19770  rinvmod  19772  mulgnn0di  19791  mulgmhm  19793  ghmcmn  19797  prdscmnd  19827  gsumres  19879  gsumcl2  19880  gsumf1o  19882  gsumsubmcl  19885  gsumadd  19889  gsumsplit  19894  gsummhm  19904  gsummulglem  19907  gsuminv  19912  gsumpr  19921  gsumunsnfd  19923  gsumdifsnd  19927  gsum2d  19938  prdsgsum  19947  gsumle  20111  srgmnd  20162  gsumvsmul  20912  xrge0omnd  21435  frlmgsum  21762  frlmup2  21789  islindf4  21828  evlslem3  22068  mdetdiagid  22575  mdetrlin  22577  gsummatr01lem3  22632  gsummatr01  22634  chpscmat  22817  chp0mat  22821  chpidmat  22822  tmdgsum  24070  tmdgsum2  24071  tsms0  24117  tsmsmhm  24121  tsmsadd  24122  tgptsmscls  24125  tsmssplit  24127  tsmsxplem1  24128  tsmsxplem2  24129  imasdsf1olem  24348  lgseisenlem4  27355  xrge00  33089  gsumvsmul1  33127  gsummptres  33128  slmdmnd  33282  psrmonprod  33711  lbsdiflsp0  33786  xrge0iifmhm  34099  xrge0tmdALT  34106  esum0  34209  esumsnf  34224  esumcocn  34240  aks6d1c1  42569  aks6d1c5lem0  42588  aks6d1c5lem3  42590  aks6d1c5lem2  42591  aks6d1c5  42592  gsumge0cl  46817  sge0tsms  46826  gsumdifsndf  48669