Theorem cmnmnd 19734

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  Mndcmnd 18668  CMndccmn 19717

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-cmn 19719

This theorem is referenced by:  cmn32  19737  cmn4  19738  cmn12  19739  cmnmndd  19741  rinvmod  19743  mulgnn0di  19762  mulgmhm  19764  ghmcmn  19768  prdscmnd  19798  gsumres  19850  gsumcl2  19851  gsumf1o  19853  gsumsubmcl  19856  gsumadd  19860  gsumsplit  19865  gsummhm  19875  gsummulglem  19878  gsuminv  19883  gsumpr  19892  gsumunsnfd  19894  gsumdifsnd  19898  gsum2d  19909  prdsgsum  19918  srgmnd  20106  gsumvsmul  20839  frlmgsum  21688  frlmup2  21715  islindf4  21754  evlslem3  21994  mdetdiagid  22494  mdetrlin  22496  gsummatr01lem3  22551  gsummatr01  22553  chpscmat  22736  chp0mat  22740  chpidmat  22741  tmdgsum  23989  tmdgsum2  23990  tsms0  24036  tsmsmhm  24040  tsmsadd  24041  tgptsmscls  24044  tsmssplit  24046  tsmsxplem1  24047  tsmsxplem2  24048  imasdsf1olem  24268  lgseisenlem4  27296  xrge00  32960  gsumvsmul1  32998  gsummptres  32999  xrge0omnd  33032  gsumle  33045  slmdmnd  33166  lbsdiflsp0  33629  xrge0iifmhm  33936  xrge0tmdALT  33943  esum0  34046  esumsnf  34061  esumcocn  34077  aks6d1c1  42111  aks6d1c5lem0  42130  aks6d1c5lem3  42132  aks6d1c5lem2  42133  aks6d1c5  42134  gsumge0cl  46376  sge0tsms  46385  gsumdifsndf  48173