Theorem cmnmnd 20004

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ‘cfv 6537  (class class class)co 7418  Basecbs 17380  +_gcplusg 17421  Mndcmnd 18916  CMndccmn 19987

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-cmn 19989

This theorem is used by:  cmn32  20007  cmn4  20008  cmn12  20009  cmnmndd  20011  rinvmod  20013  mulgnn0di  20032  mulgmhm  20034  ghmcmn  20038  prdscmnd  20068  gsumres  20120  gsumcl2  20121  gsumf1o  20123  gsumsubmcl  20126  gsumadd  20130  gsumsplit  20135  gsummhm  20145  gsummulglem  20148  gsuminv  20153  gsumpr  20162  gsumunsnfd  20164  gsumdifsnd  20168  gsum2d  20179  prdsgsum  20188  gsumle  20352  srgmnd  20409  gsumvsmul  21194  xrge0omnd  21744  frlmgsum  22071  frlmup2  22098  islindf4  22137  evlslem3  22382  mdetdiagid  22908  mdetrlin  22910  gsummatr01lem3  22965  gsummatr01  22967  chpscmat  23153  chp0mat  23157  chpidmat  23158  tmdgsum  24407  tmdgsum2  24408  tsms0  24454  tsmsmhm  24458  tsmsadd  24459  tgptsmscls  24462  tsmssplit  24464  tsmsxplem1  24465  tsmsxplem2  24466  imasdsf1olem  24685  lgseisenlem4  27698  xrge00  33568  gsumvsmul1  33605  gsummptres  33606  slmdmnd  33760  psrmonprod  34177  lbsdiflsp0  34251  xrge0iifmhm  34564  xrge0tmdALT  34571  esum0  34674  esumsnf  34689  esumcocn  34705  aks6d1c1  43146  aks6d1c5lem0  43165  aks6d1c5lem3  43167  aks6d1c5lem2  43168  aks6d1c5  43169  gsumge0cl  47350  sge0tsms  47359  gsumdifsndf  49247