Theorem cmnmnd 19706

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ∀wral 3059  ‘cfv 6542  (class class class)co 7411  Basecbs 17148  +_gcplusg 17201  Mndcmnd 18659  CMndccmn 19689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-cmn 19691

This theorem is referenced by:  cmn32  19709  cmn4  19710  cmn12  19711  cmnmndd  19713  rinvmod  19715  mulgnn0di  19734  mulgmhm  19736  ghmcmn  19740  prdscmnd  19770  gsumres  19822  gsumcl2  19823  gsumf1o  19825  gsumsubmcl  19828  gsumadd  19832  gsumsplit  19837  gsummhm  19847  gsummulglem  19850  gsuminv  19855  gsumpr  19864  gsumunsnfd  19866  gsumdifsnd  19870  gsum2d  19881  prdsgsum  19890  srgmnd  20084  gsumvsmul  20680  frlmgsum  21546  frlmup2  21573  islindf4  21612  evlslem3  21862  mdetdiagid  22322  mdetrlin  22324  gsummatr01lem3  22379  gsummatr01  22381  chpscmat  22564  chp0mat  22568  chpidmat  22569  tmdgsum  23819  tmdgsum2  23820  tsms0  23866  tsmsmhm  23870  tsmsadd  23871  tgptsmscls  23874  tsmssplit  23876  tsmsxplem1  23877  tsmsxplem2  23878  imasdsf1olem  24099  lgseisenlem4  27117  xrge00  32454  gsumvsmul1  32473  gsummptres  32474  xrge0omnd  32499  gsumle  32512  slmdmnd  32621  lbsdiflsp0  32999  xrge0iifmhm  33217  xrge0tmdALT  33224  esum0  33345  esumsnf  33360  esumcocn  33376  gsumge0cl  45385  sge0tsms  45394  gsumdifsndf  46857