Theorem cmnmnd 19713

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ‘cfv 6488  (class class class)co 7354  Basecbs 17124  +_gcplusg 17165  Mndcmnd 18646  CMndccmn 19696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6444  df-fv 6496  df-ov 7357  df-cmn 19698

This theorem is referenced by:  cmn32  19716  cmn4  19717  cmn12  19718  cmnmndd  19720  rinvmod  19722  mulgnn0di  19741  mulgmhm  19743  ghmcmn  19747  prdscmnd  19777  gsumres  19829  gsumcl2  19830  gsumf1o  19832  gsumsubmcl  19835  gsumadd  19839  gsumsplit  19844  gsummhm  19854  gsummulglem  19857  gsuminv  19862  gsumpr  19871  gsumunsnfd  19873  gsumdifsnd  19877  gsum2d  19888  prdsgsum  19897  gsumle  20061  srgmnd  20112  gsumvsmul  20863  xrge0omnd  21386  frlmgsum  21713  frlmup2  21740  islindf4  21779  evlslem3  22018  mdetdiagid  22518  mdetrlin  22520  gsummatr01lem3  22575  gsummatr01  22577  chpscmat  22760  chp0mat  22764  chpidmat  22765  tmdgsum  24013  tmdgsum2  24014  tsms0  24060  tsmsmhm  24064  tsmsadd  24065  tgptsmscls  24068  tsmssplit  24070  tsmsxplem1  24071  tsmsxplem2  24072  imasdsf1olem  24291  lgseisenlem4  27319  xrge00  33004  gsumvsmul1  33040  gsummptres  33041  slmdmnd  33184  lbsdiflsp0  33662  xrge0iifmhm  33975  xrge0tmdALT  33982  esum0  34085  esumsnf  34100  esumcocn  34116  aks6d1c1  42232  aks6d1c5lem0  42251  aks6d1c5lem3  42253  aks6d1c5lem2  42254  aks6d1c5  42255  gsumge0cl  46496  sge0tsms  46505  gsumdifsndf  48308