Theorem cmnmndd 19710

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18637  CMndccmn 19686

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-cmn 19688

This theorem is referenced by:  psrbagev1  21960  evlslem1  21965  psdadd  22026  evls1fpws  22232  mdetrsca  22466  cmn246135  32947  cmn145236  32948  gsummptres2  32966  gsumfs2d  32968  gsumtp  32971  gsumhashmul  32974  gsumwun  32978  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  elrspunidl  33372  elrspunsn  33373  rprmdvdsprod  33478  dfufd2lem  33493  fldextrspunlsplem  33641  fldextrspunlsp  33642  isprimroot2  42055  primrootsunit1  42058  primrootscoprmpow  42060  primrootscoprbij  42063  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1p7  42074  aks6d1c1p6  42075  aks6d1c1  42077  aks6d1c2lem4  42088  aks6d1c5lem0  42096  aks6d1c5lem2  42099  aks6d1c5  42100  aks5lem3a  42150  unitscyglem5  42160  pwsgprod  42505  evlsvvval  42524  selvvvval  42546