Theorem cmnmnd 19839

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  Mndcmnd 18772  CMndccmn 19822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-cmn 19824

This theorem is referenced by:  cmn32  19842  cmn4  19843  cmn12  19844  cmnmndd  19846  rinvmod  19848  mulgnn0di  19867  mulgmhm  19869  ghmcmn  19873  prdscmnd  19903  gsumres  19955  gsumcl2  19956  gsumf1o  19958  gsumsubmcl  19961  gsumadd  19965  gsumsplit  19970  gsummhm  19980  gsummulglem  19983  gsuminv  19988  gsumpr  19997  gsumunsnfd  19999  gsumdifsnd  20003  gsum2d  20014  prdsgsum  20023  srgmnd  20217  gsumvsmul  20946  frlmgsum  21815  frlmup2  21842  islindf4  21881  evlslem3  22127  mdetdiagid  22627  mdetrlin  22629  gsummatr01lem3  22684  gsummatr01  22686  chpscmat  22869  chp0mat  22873  chpidmat  22874  tmdgsum  24124  tmdgsum2  24125  tsms0  24171  tsmsmhm  24175  tsmsadd  24176  tgptsmscls  24179  tsmssplit  24181  tsmsxplem1  24182  tsmsxplem2  24183  imasdsf1olem  24404  lgseisenlem4  27440  xrge00  32998  gsumvsmul1  33034  gsummptres  33035  xrge0omnd  33061  gsumle  33074  slmdmnd  33185  lbsdiflsp0  33639  xrge0iifmhm  33885  xrge0tmdALT  33892  esum0  34013  esumsnf  34028  esumcocn  34044  aks6d1c1  42073  aks6d1c5lem0  42092  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c5  42096  gsumge0cl  46292  sge0tsms  46301  gsumdifsndf  47904