Theorem cmnmndd 19711

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

Syntax hints:   → wi 4   ∈ wcel 2111  Mndcmnd 18637  CMndccmn 19687

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-cmn 19689

This theorem is referenced by:  psrbagev1  22007  evlslem1  22012  psdadd  22073  evls1fpws  22279  mdetrsca  22513  cmn246135  33006  cmn145236  33007  gsummptres2  33025  gsumfs2d  33027  gsumtp  33030  gsumhashmul  33033  gsumwun  33037  elrgspnlem1  33201  elrgspnlem2  33202  elrgspnsubrunlem1  33206  elrgspnsubrunlem2  33207  elrspunidl  33385  elrspunsn  33386  rprmdvdsprod  33491  dfufd2lem  33506  fldextrspunlsplem  33678  fldextrspunlsp  33679  extdgfialglem2  33698  isprimroot2  42127  primrootsunit1  42130  primrootscoprmpow  42132  primrootscoprbij  42135  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1p7  42146  aks6d1c1p6  42147  aks6d1c1  42149  aks6d1c2lem4  42160  aks6d1c5lem0  42168  aks6d1c5lem2  42171  aks6d1c5  42172  aks5lem3a  42222  unitscyglem5  42232  pwsgprod  42577  evlsvvval  42596  selvvvval  42618