Theorem cmnmnd 19855

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ‘cfv 6525  (class class class)co 7400  Basecbs 17257  +_gcplusg 17298  Mndcmnd 18780  CMndccmn 19838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-iota 6481  df-fv 6533  df-ov 7403  df-cmn 19840

This theorem is referenced by:  cmn32  19858  cmn4  19859  cmn12  19860  cmnmndd  19862  rinvmod  19864  mulgnn0di  19883  mulgmhm  19885  ghmcmn  19889  prdscmnd  19919  gsumres  19971  gsumcl2  19972  gsumf1o  19974  gsumsubmcl  19977  gsumadd  19981  gsumsplit  19986  gsummhm  19996  gsummulglem  19999  gsuminv  20004  gsumpr  20013  gsumunsnfd  20015  gsumdifsnd  20019  gsum2d  20030  prdsgsum  20039  gsumle  20203  srgmnd  20260  gsumvsmul  21013  xrge0omnd  21552  frlmgsum  21879  frlmup2  21906  islindf4  21945  evlslem3  22188  mdetdiagid  22714  mdetrlin  22716  gsummatr01lem3  22771  gsummatr01  22773  chpscmat  22956  chp0mat  22960  chpidmat  22961  tmdgsum  24209  tmdgsum2  24210  tsms0  24256  tsmsmhm  24260  tsmsadd  24261  tgptsmscls  24264  tsmssplit  24266  tsmsxplem1  24267  tsmsxplem2  24268  imasdsf1olem  24487  lgseisenlem4  27496  xrge00  33242  gsumvsmul1  33279  gsummptres  33280  slmdmnd  33434  psrmonprod  33854  lbsdiflsp0  33928  xrge0iifmhm  34241  xrge0tmdALT  34248  esum0  34351  esumsnf  34366  esumcocn  34382  aks6d1c1  42740  aks6d1c5lem0  42759  aks6d1c5lem3  42761  aks6d1c5lem2  42762  aks6d1c5  42763  gsumge0cl  46944  sge0tsms  46953  gsumdifsndf  48802