Theorem cmnmnd 19665

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  +_gcplusg 17197  Mndcmnd 18625  CMndccmn 19648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-cmn 19650

This theorem is referenced by:  cmn32  19668  cmn4  19669  cmn12  19670  cmnmndd  19672  rinvmod  19674  mulgnn0di  19693  mulgmhm  19695  ghmcmn  19699  prdscmnd  19729  gsumres  19781  gsumcl2  19782  gsumf1o  19784  gsumsubmcl  19787  gsumadd  19791  gsumsplit  19796  gsummhm  19806  gsummulglem  19809  gsuminv  19814  gsumpr  19823  gsumunsnfd  19825  gsumdifsnd  19829  gsum2d  19840  prdsgsum  19849  srgmnd  20013  gsumvsmul  20536  frlmgsum  21327  frlmup2  21354  islindf4  21393  evlslem3  21643  mdetdiagid  22102  mdetrlin  22104  gsummatr01lem3  22159  gsummatr01  22161  chpscmat  22344  chp0mat  22348  chpidmat  22349  tmdgsum  23599  tmdgsum2  23600  tsms0  23646  tsmsmhm  23650  tsmsadd  23651  tgptsmscls  23654  tsmssplit  23656  tsmsxplem1  23657  tsmsxplem2  23658  imasdsf1olem  23879  lgseisenlem4  26881  xrge00  32187  gsumvsmul1  32203  gsummptres  32204  xrge0omnd  32229  gsumle  32242  slmdmnd  32351  lbsdiflsp0  32711  xrge0iifmhm  32919  xrge0tmdALT  32926  esum0  33047  esumsnf  33062  esumcocn  33078  gsumge0cl  45087  sge0tsms  45096  gsumdifsndf  46591