Theorem cmnmnd 19733

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 19725	. 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 6513  (class class class)co 7389  Basecbs 17185  +_gcplusg 17226  Mndcmnd 18667  CMndccmn 19716

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 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392  df-cmn 19718

This theorem is referenced by:  cmn32  19736  cmn4  19737  cmn12  19738  cmnmndd  19740  rinvmod  19742  mulgnn0di  19761  mulgmhm  19763  ghmcmn  19767  prdscmnd  19797  gsumres  19849  gsumcl2  19850  gsumf1o  19852  gsumsubmcl  19855  gsumadd  19859  gsumsplit  19864  gsummhm  19874  gsummulglem  19877  gsuminv  19882  gsumpr  19891  gsumunsnfd  19893  gsumdifsnd  19897  gsum2d  19908  prdsgsum  19917  srgmnd  20105  gsumvsmul  20838  frlmgsum  21687  frlmup2  21714  islindf4  21753  evlslem3  21993  mdetdiagid  22493  mdetrlin  22495  gsummatr01lem3  22550  gsummatr01  22552  chpscmat  22735  chp0mat  22739  chpidmat  22740  tmdgsum  23988  tmdgsum2  23989  tsms0  24035  tsmsmhm  24039  tsmsadd  24040  tgptsmscls  24043  tsmssplit  24045  tsmsxplem1  24046  tsmsxplem2  24047  imasdsf1olem  24267  lgseisenlem4  27295  xrge00  32959  gsumvsmul1  32997  gsummptres  32998  xrge0omnd  33031  gsumle  33044  slmdmnd  33165  lbsdiflsp0  33628  xrge0iifmhm  33935  xrge0tmdALT  33942  esum0  34045  esumsnf  34060  esumcocn  34076  aks6d1c1  42099  aks6d1c5lem0  42118  aks6d1c5lem3  42120  aks6d1c5lem2  42121  aks6d1c5  42122  gsumge0cl  46362  sge0tsms  46371  gsumdifsndf  48159