Theorem cmnmndd 19785

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18712  CMndccmn 19761

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-cmn 19763

This theorem is referenced by:  psrbagev1  22035  evlslem1  22040  psdadd  22101  evls1fpws  22307  mdetrsca  22541  cmn246135  33028  cmn145236  33029  gsummptres2  33047  gsumfs2d  33049  gsumtp  33052  gsumhashmul  33055  gsumwun  33059  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnsubrunlem1  33242  elrgspnsubrunlem2  33243  elrspunidl  33443  elrspunsn  33444  rprmdvdsprod  33549  dfufd2lem  33564  fldextrspunlsplem  33714  fldextrspunlsp  33715  isprimroot2  42107  primrootsunit1  42110  primrootscoprmpow  42112  primrootscoprbij  42115  aks6d1c1p3  42123  aks6d1c1p4  42124  aks6d1c1p5  42125  aks6d1c1p7  42126  aks6d1c1p6  42127  aks6d1c1  42129  aks6d1c2lem4  42140  aks6d1c5lem0  42148  aks6d1c5lem2  42151  aks6d1c5  42152  aks5lem3a  42202  unitscyglem5  42212  pwsgprod  42567  evlsvvval  42586  selvvvval  42608