Theorem cmnmnd 18605

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  ∀wral 3090  ‘cfv 6137  (class class class)co 6924  Basecbs 16266  +_gcplusg 16349  Mndcmnd 17691  CMndccmn 18590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-iota 6101  df-fv 6145  df-ov 6927  df-cmn 18592

This theorem is referenced by:  cmn32  18608  cmn4  18609  cmn12  18610  mulgnn0di  18628  mulgmhm  18630  ghmcmn  18634  prdscmnd  18661  gsumres  18711  gsumcl2  18712  gsumf1o  18714  gsumsubmcl  18716  gsumadd  18720  gsumsplit  18725  gsummhm  18735  gsummulglem  18738  gsuminv  18743  gsumunsnfd  18753  gsumdifsnd  18757  gsum2d  18768  prdsgsum  18774  srgmnd  18907  gsumvsmul  19330  psrbagev1  19917  evlslem3  19921  evlslem1  19922  frlmgsum  20526  frlmup2  20553  islindf4  20592  mdetdiagid  20822  mdetrlin  20824  mdetrsca  20825  gsummatr01lem3  20880  gsummatr01  20882  chpscmat  21065  chp0mat  21069  chpidmat  21070  tmdgsum  22318  tmdgsum2  22319  tsms0  22364  tsmsmhm  22368  tsmsadd  22369  tgptsmscls  22372  tsmssplit  22374  tsmsxplem1  22375  tsmsxplem2  22376  imasdsf1olem  22597  lgseisenlem4  25566  xrge00  30256  xrge0omnd  30281  slmdmnd  30329  gsumle  30349  gsummptres  30354  lbsdiflsp0  30448  xrge0iifmhm  30591  xrge0tmdOLD  30597  esum0  30717  esumsnf  30732  esumcocn  30748  gsumge0cl  41526  sge0tsms  41535  gsumpr  43168  gsumdifsndf  43173