Theorem cmnmnd 18031

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  Mndcmnd 17117  CMndccmn 18016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-cmn 18018

This theorem is referenced by:  cmn32  18034  cmn4  18035  cmn12  18036  mulgnn0di  18054  mulgmhm  18056  ghmcmn  18060  prdscmnd  18087  gsumres  18137  gsumcl2  18138  gsumf1o  18140  gsumsubmcl  18142  gsumadd  18146  gsumsplit  18151  gsummhm  18161  gsummulglem  18164  gsuminv  18169  gsumunsnfd  18179  gsumdifsnd  18183  gsum2d  18194  prdsgsum  18200  srgmnd  18332  gsumvsmul  18750  psrbagev1  19331  evlslem3  19335  evlslem1  19336  frlmgsum  19930  frlmup2  19957  islindf4  19996  mdetdiagid  20225  mdetrlin  20227  mdetrsca  20228  gsummatr01lem3  20282  gsummatr01  20284  chpscmat  20466  chp0mat  20470  chpidmat  20471  tmdgsum  21709  tmdgsum2  21710  tsms0  21755  tsmsmhm  21759  tsmsadd  21760  tgptsmscls  21763  tsmssplit  21765  tsmsxplem1  21766  tsmsxplem2  21767  imasdsf1olem  21988  lgseisenlem4  24903  xrge00  29017  xrge0omnd  29042  slmdmnd  29090  gsumle  29110  gsummptres  29115  xrge0iifmhm  29313  xrge0tmdOLD  29319  esum0  29438  esumsnf  29453  esumcocn  29469  gsumge0cl  39264  sge0tsms  39273  gsumpr  41932  gsumdifsndf  41937