Theorem cmnmndd 19745

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18671  CMndccmn 19721

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-cmn 19723

This theorem is referenced by:  pwsgprod  20277  psrbagev1  22044  evlslem1  22049  evlsvvval  22060  psdadd  22118  evls1fpws  22325  mdetrsca  22559  cmn246135  33125  cmn145236  33126  gsummptres2  33146  gsummptfzsplitra  33151  gsummptfzsplitla  33152  gsumfs2d  33154  gsumtp  33157  gsumhashmul  33160  gsumwun  33169  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrspunidl  33520  elrspunsn  33521  rprmdvdsprod  33626  dfufd2lem  33641  evlextv  33718  esplyfvaln  33750  vietalem  33755  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem2  33870  isprimroot2  42461  primrootsunit1  42464  primrootscoprmpow  42466  primrootscoprbij  42469  aks6d1c1p3  42477  aks6d1c1p4  42478  aks6d1c1p5  42479  aks6d1c1p7  42480  aks6d1c1p6  42481  aks6d1c1  42483  aks6d1c2lem4  42494  aks6d1c5lem0  42502  aks6d1c5lem2  42505  aks6d1c5  42506  aks5lem3a  42556  unitscyglem5  42566  selvvvval  42940