Theorem cmnmndd 19798

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

Syntax hints:   → wi 4   ∈ wcel 2099  Mndcmnd 18722  CMndccmn 19774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-iota 6498  df-fv 6554  df-ov 7419  df-cmn 19776

This theorem is referenced by:  psrbagev1  22086  psrbagev1OLD  22087  evlslem1  22093  psdadd  22153  evls1fpws  22357  mdetrsca  22593  cmn246135  32909  cmn145236  32910  gsummptres2  32925  gsumtp  32928  gsumhashmul  32929  elrspunidl  33309  elrspunsn  33310  rprmdvdsprod  33415  dfufd2lem  33430  isprimroot2  41806  primrootsunit1  41809  primrootscoprmpow  41811  primrootscoprbij  41814  aks6d1c1p3  41822  aks6d1c1p4  41823  aks6d1c1p5  41824  aks6d1c1p7  41825  aks6d1c1p6  41826  aks6d1c1  41828  aks6d1c2lem4  41839  aks6d1c5lem0  41847  aks6d1c5lem2  41850  aks6d1c5  41851  aks5lem3a  41901  pwsgprod  42234  evlsvvval  42253  selvvvval  42275