Theorem cmnmnd 19694

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  Mndcmnd 18626  CMndccmn 19677

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-cmn 19679

This theorem is referenced by:  cmn32  19697  cmn4  19698  cmn12  19699  cmnmndd  19701  rinvmod  19703  mulgnn0di  19722  mulgmhm  19724  ghmcmn  19728  prdscmnd  19758  gsumres  19810  gsumcl2  19811  gsumf1o  19813  gsumsubmcl  19816  gsumadd  19820  gsumsplit  19825  gsummhm  19835  gsummulglem  19838  gsuminv  19843  gsumpr  19852  gsumunsnfd  19854  gsumdifsnd  19858  gsum2d  19869  prdsgsum  19878  gsumle  20042  srgmnd  20093  gsumvsmul  20847  xrge0omnd  21370  frlmgsum  21697  frlmup2  21724  islindf4  21763  evlslem3  22003  mdetdiagid  22503  mdetrlin  22505  gsummatr01lem3  22560  gsummatr01  22562  chpscmat  22745  chp0mat  22749  chpidmat  22750  tmdgsum  23998  tmdgsum2  23999  tsms0  24045  tsmsmhm  24049  tsmsadd  24050  tgptsmscls  24053  tsmssplit  24055  tsmsxplem1  24056  tsmsxplem2  24057  imasdsf1olem  24277  lgseisenlem4  27305  xrge00  32981  gsumvsmul1  33017  gsummptres  33018  slmdmnd  33161  lbsdiflsp0  33601  xrge0iifmhm  33908  xrge0tmdALT  33915  esum0  34018  esumsnf  34033  esumcocn  34049  aks6d1c1  42092  aks6d1c5lem0  42111  aks6d1c5lem3  42113  aks6d1c5lem2  42114  aks6d1c5  42115  gsumge0cl  46356  sge0tsms  46365  gsumdifsndf  48169