Theorem cmnmndd 19897

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Mndcmnd 18813  CMndccmn 19873

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-cmn 19875

This theorem is used by:  pwsgprod  20436  psrbagev1  22257  evlslem1  22262  evlsvvval  22273  selvvvval  22322  psdadd  22355  evls1fpws  22558  mdetrsca  22789  cmn246135  33376  cmn145236  33377  gsummptres2  33396  gsummptfzsplitra  33401  gsummptfzsplitla  33402  gsumfs2d  33404  gsumtp  33407  gsumhashmul  33410  gsumwun  33419  elrgspnlem1  33585  elrgspnlem2  33586  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  elrspunidl  33759  elrspunsn  33760  rprmdvdsprod  33847  dfufd2lem  33862  evlextv  33955  esplyfvaln  33987  vietalem  33992  fldextrspunlsplem  34086  fldextrspunlsp  34087  extdgfialglem2  34106  isprimroot2  42894  primrootsunit1  42897  primrootscoprmpow  42899  primrootscoprbij  42902  aks6d1c1p3  42910  aks6d1c1p4  42911  aks6d1c1p5  42912  aks6d1c1p7  42913  aks6d1c1p6  42914  aks6d1c1  42916  aks6d1c2lem4  42927  aks6d1c5lem0  42935  aks6d1c5lem2  42938  aks6d1c5  42939  aks5lem3a  42989  unitscyglem5  42999