Theorem cmnmnd 19726

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  +_gcplusg 17177  Mndcmnd 18659  CMndccmn 19709

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-cmn 19711

This theorem is referenced by:  cmn32  19729  cmn4  19730  cmn12  19731  cmnmndd  19733  rinvmod  19735  mulgnn0di  19754  mulgmhm  19756  ghmcmn  19760  prdscmnd  19790  gsumres  19842  gsumcl2  19843  gsumf1o  19845  gsumsubmcl  19848  gsumadd  19852  gsumsplit  19857  gsummhm  19867  gsummulglem  19870  gsuminv  19875  gsumpr  19884  gsumunsnfd  19886  gsumdifsnd  19890  gsum2d  19901  prdsgsum  19910  gsumle  20074  srgmnd  20125  gsumvsmul  20877  xrge0omnd  21400  frlmgsum  21727  frlmup2  21754  islindf4  21793  evlslem3  22035  mdetdiagid  22544  mdetrlin  22546  gsummatr01lem3  22601  gsummatr01  22603  chpscmat  22786  chp0mat  22790  chpidmat  22791  tmdgsum  24039  tmdgsum2  24040  tsms0  24086  tsmsmhm  24090  tsmsadd  24091  tgptsmscls  24094  tsmssplit  24096  tsmsxplem1  24097  tsmsxplem2  24098  imasdsf1olem  24317  lgseisenlem4  27345  xrge00  33096  gsumvsmul1  33134  gsummptres  33135  slmdmnd  33288  lbsdiflsp0  33783  xrge0iifmhm  34096  xrge0tmdALT  34103  esum0  34206  esumsnf  34221  esumcocn  34237  aks6d1c1  42370  aks6d1c5lem0  42389  aks6d1c5lem3  42391  aks6d1c5lem2  42392  aks6d1c5  42393  gsumge0cl  46615  sge0tsms  46624  gsumdifsndf  48427