Theorem cmnmndd 19770

Description: A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)

Hypothesis

Ref	Expression
cmnmndd.1	⊢ (𝜑 → 𝐺 ∈ CMnd)

Assertion

Ref	Expression
cmnmndd	⊢ (𝜑 → 𝐺 ∈ Mnd)

Proof of Theorem cmnmndd

Step	Hyp	Ref	Expression
1		cmnmndd.1	. 2 ⊢ (𝜑 → 𝐺 ∈ CMnd)
2		cmnmnd 19763	. 2 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18693  CMndccmn 19746

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-cmn 19748

This theorem is referenced by:  pwsgprod  20300  psrbagev1  22065  evlslem1  22070  evlsvvval  22081  psdadd  22139  evls1fpws  22344  mdetrsca  22578  cmn246135  33108  cmn145236  33109  gsummptres2  33129  gsummptfzsplitra  33134  gsummptfzsplitla  33135  gsumfs2d  33137  gsumtp  33140  gsumhashmul  33143  gsumwun  33152  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrspunidl  33503  elrspunsn  33504  rprmdvdsprod  33609  dfufd2lem  33624  evlextv  33701  esplyfvaln  33733  vietalem  33738  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem2  33853  isprimroot2  42547  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1p7  42566  aks6d1c1p6  42567  aks6d1c1  42569  aks6d1c2lem4  42580  aks6d1c5lem0  42588  aks6d1c5lem2  42591  aks6d1c5  42592  aks5lem3a  42642  unitscyglem5  42652  selvvvval  43032