Theorem cmnmnd 19727

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 19719	. 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 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  Mndcmnd 18661  CMndccmn 19710

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-cmn 19712

This theorem is referenced by:  cmn32  19730  cmn4  19731  cmn12  19732  cmnmndd  19734  rinvmod  19736  mulgnn0di  19755  mulgmhm  19757  ghmcmn  19761  prdscmnd  19791  gsumres  19843  gsumcl2  19844  gsumf1o  19846  gsumsubmcl  19849  gsumadd  19853  gsumsplit  19858  gsummhm  19868  gsummulglem  19871  gsuminv  19876  gsumpr  19885  gsumunsnfd  19887  gsumdifsnd  19891  gsum2d  19902  prdsgsum  19911  srgmnd  20099  gsumvsmul  20832  frlmgsum  21681  frlmup2  21708  islindf4  21747  evlslem3  21987  mdetdiagid  22487  mdetrlin  22489  gsummatr01lem3  22544  gsummatr01  22546  chpscmat  22729  chp0mat  22733  chpidmat  22734  tmdgsum  23982  tmdgsum2  23983  tsms0  24029  tsmsmhm  24033  tsmsadd  24034  tgptsmscls  24037  tsmssplit  24039  tsmsxplem1  24040  tsmsxplem2  24041  imasdsf1olem  24261  lgseisenlem4  27289  xrge00  32953  gsumvsmul1  32991  gsummptres  32992  xrge0omnd  33025  gsumle  33038  slmdmnd  33159  lbsdiflsp0  33622  xrge0iifmhm  33929  xrge0tmdALT  33936  esum0  34039  esumsnf  34054  esumcocn  34070  aks6d1c1  42104  aks6d1c5lem0  42123  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c5  42127  gsumge0cl  46369  sge0tsms  46378  gsumdifsndf  48169