Theorem cmnmndd 19724

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 19717	. 2 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2113  Mndcmnd 18650  CMndccmn 19700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-cmn 19702

This theorem is referenced by:  pwsgprod  20256  psrbagev1  22023  evlslem1  22028  evlsvvval  22039  psdadd  22097  evls1fpws  22304  mdetrsca  22538  cmn246135  33043  cmn145236  33044  gsummptres2  33064  gsummptfzsplitra  33069  gsummptfzsplitla  33070  gsumfs2d  33072  gsumtp  33075  gsumhashmul  33078  gsumwun  33086  elrgspnlem1  33252  elrgspnlem2  33253  elrgspnsubrunlem1  33257  elrgspnsubrunlem2  33258  elrspunidl  33437  elrspunsn  33438  rprmdvdsprod  33543  dfufd2lem  33558  evlextv  33635  vietalem  33663  fldextrspunlsplem  33758  fldextrspunlsp  33759  extdgfialglem2  33778  isprimroot2  42260  primrootsunit1  42263  primrootscoprmpow  42265  primrootscoprbij  42268  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1p7  42279  aks6d1c1p6  42280  aks6d1c1  42282  aks6d1c2lem4  42293  aks6d1c5lem0  42301  aks6d1c5lem2  42304  aks6d1c5  42305  aks5lem3a  42355  unitscyglem5  42365  selvvvval  42743