Theorem cmnmnd 18522

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

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  ∀wral 3090  ‘cfv 6102  (class class class)co 6879  Basecbs 16183  +_gcplusg 16266  Mndcmnd 17608  CMndccmn 18507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-br 4845  df-iota 6065  df-fv 6110  df-ov 6882  df-cmn 18509

This theorem is referenced by:  cmn32  18525  cmn4  18526  cmn12  18527  mulgnn0di  18545  mulgmhm  18547  ghmcmn  18551  prdscmnd  18578  gsumres  18628  gsumcl2  18629  gsumf1o  18631  gsumsubmcl  18633  gsumadd  18637  gsumsplit  18642  gsummhm  18652  gsummulglem  18655  gsuminv  18660  gsumunsnfd  18670  gsumdifsnd  18674  gsum2d  18685  prdsgsum  18691  srgmnd  18824  gsumvsmul  19244  psrbagev1  19831  evlslem3  19835  evlslem1  19836  frlmgsum  20435  frlmup2  20462  islindf4  20501  mdetdiagid  20731  mdetrlin  20733  mdetrsca  20734  gsummatr01lem3  20789  gsummatr01  20791  chpscmat  20974  chp0mat  20978  chpidmat  20979  tmdgsum  22226  tmdgsum2  22227  tsms0  22272  tsmsmhm  22276  tsmsadd  22277  tgptsmscls  22280  tsmssplit  22282  tsmsxplem1  22283  tsmsxplem2  22284  imasdsf1olem  22505  lgseisenlem4  25454  xrge00  30201  xrge0omnd  30226  slmdmnd  30274  gsumle  30294  gsummptres  30299  xrge0iifmhm  30500  xrge0tmdOLD  30506  esum0  30626  esumsnf  30641  esumcocn  30657  gsumge0cl  41326  sge0tsms  41335  gsumpr  42933  gsumdifsndf  42938