Theorem cmnmnd 19868

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  Mndcmnd 18793  CMndccmn 19851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-cmn 19853

This theorem is referenced by:  cmn32  19871  cmn4  19872  cmn12  19873  cmnmndd  19875  rinvmod  19877  mulgnn0di  19896  mulgmhm  19898  ghmcmn  19902  prdscmnd  19932  gsumres  19984  gsumcl2  19985  gsumf1o  19987  gsumsubmcl  19990  gsumadd  19994  gsumsplit  19999  gsummhm  20009  gsummulglem  20012  gsuminv  20017  gsumpr  20026  gsumunsnfd  20028  gsumdifsnd  20032  gsum2d  20043  prdsgsum  20052  gsumle  20216  srgmnd  20273  gsumvsmul  21028  xrge0omnd  21576  frlmgsum  21903  frlmup2  21930  islindf4  21969  evlslem3  22212  mdetdiagid  22738  mdetrlin  22740  gsummatr01lem3  22795  gsummatr01  22797  chpscmat  22980  chp0mat  22984  chpidmat  22985  tmdgsum  24233  tmdgsum2  24234  tsms0  24280  tsmsmhm  24284  tsmsadd  24285  tgptsmscls  24288  tsmssplit  24290  tsmsxplem1  24291  tsmsxplem2  24292  imasdsf1olem  24511  lgseisenlem4  27523  xrge00  33315  gsumvsmul1  33352  gsummptres  33353  slmdmnd  33507  psrmonprod  33923  lbsdiflsp0  33997  xrge0iifmhm  34310  xrge0tmdALT  34317  esum0  34420  esumsnf  34435  esumcocn  34451  aks6d1c1  42864  aks6d1c5lem0  42883  aks6d1c5lem3  42885  aks6d1c5lem2  42886  aks6d1c5  42887  gsumge0cl  47068  sge0tsms  47077  gsumdifsndf  48929