Theorem cmnmnd 19815

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 19807	. 2 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g‘𝐺)𝑦) = (𝑦(+g‘𝐺)𝑥)))
4	3	simplbi 497	1 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  Mndcmnd 18747  CMndccmn 19798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-cmn 19800

This theorem is referenced by:  cmn32  19818  cmn4  19819  cmn12  19820  cmnmndd  19822  rinvmod  19824  mulgnn0di  19843  mulgmhm  19845  ghmcmn  19849  prdscmnd  19879  gsumres  19931  gsumcl2  19932  gsumf1o  19934  gsumsubmcl  19937  gsumadd  19941  gsumsplit  19946  gsummhm  19956  gsummulglem  19959  gsuminv  19964  gsumpr  19973  gsumunsnfd  19975  gsumdifsnd  19979  gsum2d  19990  prdsgsum  19999  srgmnd  20187  gsumvsmul  20924  frlmgsum  21792  frlmup2  21819  islindf4  21858  evlslem3  22104  mdetdiagid  22606  mdetrlin  22608  gsummatr01lem3  22663  gsummatr01  22665  chpscmat  22848  chp0mat  22852  chpidmat  22853  tmdgsum  24103  tmdgsum2  24104  tsms0  24150  tsmsmhm  24154  tsmsadd  24155  tgptsmscls  24158  tsmssplit  24160  tsmsxplem1  24161  tsmsxplem2  24162  imasdsf1olem  24383  lgseisenlem4  27422  xrge00  33017  gsumvsmul1  33054  gsummptres  33055  xrge0omnd  33088  gsumle  33101  slmdmnd  33212  lbsdiflsp0  33677  xrge0iifmhm  33938  xrge0tmdALT  33945  esum0  34050  esumsnf  34065  esumcocn  34081  aks6d1c1  42117  aks6d1c5lem0  42136  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks6d1c5  42140  gsumge0cl  46386  sge0tsms  46395  gsumdifsndf  48097