Theorem cmnmnd 19772

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  Mndcmnd 18702  CMndccmn 19755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-cmn 19757

This theorem is referenced by:  cmn32  19775  cmn4  19776  cmn12  19777  cmnmndd  19779  rinvmod  19781  mulgnn0di  19800  mulgmhm  19802  ghmcmn  19806  prdscmnd  19836  gsumres  19888  gsumcl2  19889  gsumf1o  19891  gsumsubmcl  19894  gsumadd  19898  gsumsplit  19903  gsummhm  19913  gsummulglem  19916  gsuminv  19921  gsumpr  19930  gsumunsnfd  19932  gsumdifsnd  19936  gsum2d  19947  prdsgsum  19956  gsumle  20120  srgmnd  20171  gsumvsmul  20921  xrge0omnd  21425  frlmgsum  21752  frlmup2  21779  islindf4  21818  evlslem3  22058  mdetdiagid  22565  mdetrlin  22567  gsummatr01lem3  22622  gsummatr01  22624  chpscmat  22807  chp0mat  22811  chpidmat  22812  tmdgsum  24060  tmdgsum2  24061  tsms0  24107  tsmsmhm  24111  tsmsadd  24112  tgptsmscls  24115  tsmssplit  24117  tsmsxplem1  24118  tsmsxplem2  24119  imasdsf1olem  24338  lgseisenlem4  27341  xrge00  33074  gsumvsmul1  33112  gsummptres  33113  slmdmnd  33267  psrmonprod  33696  lbsdiflsp0  33770  xrge0iifmhm  34083  xrge0tmdALT  34090  esum0  34193  esumsnf  34208  esumcocn  34224  aks6d1c1  42555  aks6d1c5lem0  42574  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c5  42578  gsumge0cl  46799  sge0tsms  46808  gsumdifsndf  48657