Theorem cmnmndd 19733

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

Syntax hints:   → wi 4   ∈ wcel 2113  Mndcmnd 18659  CMndccmn 19709

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-cmn 19711

This theorem is referenced by:  pwsgprod  20265  psrbagev1  22032  evlslem1  22037  evlsvvval  22048  psdadd  22106  evls1fpws  22313  mdetrsca  22547  cmn246135  33115  cmn145236  33116  gsummptres2  33136  gsummptfzsplitra  33141  gsummptfzsplitla  33142  gsumfs2d  33144  gsumtp  33147  gsumhashmul  33150  gsumwun  33158  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrspunidl  33509  elrspunsn  33510  rprmdvdsprod  33615  dfufd2lem  33630  evlextv  33707  vietalem  33735  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem2  33850  isprimroot2  42348  primrootsunit1  42351  primrootscoprmpow  42353  primrootscoprbij  42356  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  aks6d1c1p6  42368  aks6d1c1  42370  aks6d1c2lem4  42381  aks6d1c5lem0  42389  aks6d1c5lem2  42392  aks6d1c5  42393  aks5lem3a  42443  unitscyglem5  42453  selvvvval  42828