Theorem cmnmnd 19924

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ‘cfv 6533  (class class class)co 7413  Basecbs 17301  +_gcplusg 17342  Mndcmnd 18836  CMndccmn 19907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-cmn 19909

This theorem is used by:  cmn32  19927  cmn4  19928  cmn12  19929  cmnmndd  19931  rinvmod  19933  mulgnn0di  19952  mulgmhm  19954  ghmcmn  19958  prdscmnd  19988  gsumres  20040  gsumcl2  20041  gsumf1o  20043  gsumsubmcl  20046  gsumadd  20050  gsumsplit  20055  gsummhm  20065  gsummulglem  20068  gsuminv  20073  gsumpr  20082  gsumunsnfd  20084  gsumdifsnd  20088  gsum2d  20099  prdsgsum  20108  gsumle  20272  srgmnd  20329  gsumvsmul  21110  xrge0omnd  21658  frlmgsum  21985  frlmup2  22012  islindf4  22051  evlslem3  22296  mdetdiagid  22822  mdetrlin  22824  gsummatr01lem3  22879  gsummatr01  22881  chpscmat  23067  chp0mat  23071  chpidmat  23072  tmdgsum  24321  tmdgsum2  24322  tsms0  24368  tsmsmhm  24372  tsmsadd  24373  tgptsmscls  24376  tsmssplit  24378  tsmsxplem1  24379  tsmsxplem2  24380  imasdsf1olem  24599  lgseisenlem4  27614  xrge00  33454  gsumvsmul1  33491  gsummptres  33492  slmdmnd  33646  psrmonprod  34062  lbsdiflsp0  34136  xrge0iifmhm  34449  xrge0tmdALT  34456  esum0  34559  esumsnf  34574  esumcocn  34590  aks6d1c1  42982  aks6d1c5lem0  43001  aks6d1c5lem3  43003  aks6d1c5lem2  43004  aks6d1c5  43005  gsumge0cl  47199  sge0tsms  47208  gsumdifsndf  49096