Theorem cmnmnd 20017

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ‘cfv 6539  (class class class)co 7421  Basecbs 17393  +_gcplusg 17434  Mndcmnd 18929  CMndccmn 20000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-cmn 20002

This theorem is used by:  cmn32  20020  cmn4  20021  cmn12  20022  cmnmndd  20024  rinvmod  20026  mulgnn0di  20045  mulgmhm  20047  ghmcmn  20051  prdscmnd  20081  gsumres  20133  gsumcl2  20134  gsumf1o  20136  gsumsubmcl  20139  gsumadd  20143  gsumsplit  20148  gsummhm  20158  gsummulglem  20161  gsuminv  20166  gsumpr  20175  gsumunsnfd  20177  gsumdifsnd  20181  gsum2d  20192  prdsgsum  20201  gsumle  20365  srgmnd  20422  gsumvsmul  21207  xrge0omnd  21757  frlmgsum  22084  frlmup2  22111  islindf4  22150  evlslem3  22395  mdetdiagid  22921  mdetrlin  22923  gsummatr01lem3  22978  gsummatr01  22980  chpscmat  23166  chp0mat  23170  chpidmat  23171  tmdgsum  24420  tmdgsum2  24421  tsms0  24467  tsmsmhm  24471  tsmsadd  24472  tgptsmscls  24475  tsmssplit  24477  tsmsxplem1  24478  tsmsxplem2  24479  imasdsf1olem  24698  lgseisenlem4  27711  xrge00  33622  gsumvsmul1  33659  gsummptres  33660  slmdmnd  33814  psrmonprod  34231  lbsdiflsp0  34305  xrge0iifmhm  34618  xrge0tmdALT  34625  esum0  34728  esumsnf  34743  esumcocn  34759  aks6d1c1  43260  aks6d1c5lem0  43279  aks6d1c5lem3  43281  aks6d1c5lem2  43282  aks6d1c5  43283  gsumge0cl  47475  sge0tsms  47484  gsumdifsndf  49372