Theorem cmnmndd 19741

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18668  CMndccmn 19717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-cmn 19719

This theorem is referenced by:  psrbagev1  21991  evlslem1  21996  psdadd  22057  evls1fpws  22263  mdetrsca  22497  cmn246135  32981  cmn145236  32982  gsummptres2  33000  gsumfs2d  33002  gsumtp  33005  gsumhashmul  33008  gsumwun  33012  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrspunidl  33406  elrspunsn  33407  rprmdvdsprod  33512  dfufd2lem  33527  fldextrspunlsplem  33675  fldextrspunlsp  33676  isprimroot2  42089  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  aks6d1c1p3  42105  aks6d1c1p4  42106  aks6d1c1p5  42107  aks6d1c1p7  42108  aks6d1c1p6  42109  aks6d1c1  42111  aks6d1c2lem4  42122  aks6d1c5lem0  42130  aks6d1c5lem2  42133  aks6d1c5  42134  aks5lem3a  42184  unitscyglem5  42194  pwsgprod  42539  evlsvvval  42558  selvvvval  42580