Theorem cmnmnd 19738

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  Mndcmnd 18671  CMndccmn 19721

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-cmn 19723

This theorem is referenced by:  cmn32  19741  cmn4  19742  cmn12  19743  cmnmndd  19745  rinvmod  19747  mulgnn0di  19766  mulgmhm  19768  ghmcmn  19772  prdscmnd  19802  gsumres  19854  gsumcl2  19855  gsumf1o  19857  gsumsubmcl  19860  gsumadd  19864  gsumsplit  19869  gsummhm  19879  gsummulglem  19882  gsuminv  19887  gsumpr  19896  gsumunsnfd  19898  gsumdifsnd  19902  gsum2d  19913  prdsgsum  19922  gsumle  20086  srgmnd  20137  gsumvsmul  20889  xrge0omnd  21412  frlmgsum  21739  frlmup2  21766  islindf4  21805  evlslem3  22047  mdetdiagid  22556  mdetrlin  22558  gsummatr01lem3  22613  gsummatr01  22615  chpscmat  22798  chp0mat  22802  chpidmat  22803  tmdgsum  24051  tmdgsum2  24052  tsms0  24098  tsmsmhm  24102  tsmsadd  24103  tgptsmscls  24106  tsmssplit  24108  tsmsxplem1  24109  tsmsxplem2  24110  imasdsf1olem  24329  lgseisenlem4  27357  xrge00  33106  gsumvsmul1  33144  gsummptres  33145  slmdmnd  33299  psrmonprod  33728  lbsdiflsp0  33803  xrge0iifmhm  34116  xrge0tmdALT  34123  esum0  34226  esumsnf  34241  esumcocn  34257  aks6d1c1  42483  aks6d1c5lem0  42502  aks6d1c5lem3  42504  aks6d1c5lem2  42505  aks6d1c5  42506  gsumge0cl  46726  sge0tsms  46735  gsumdifsndf  48538