Theorem cmnmndd 19875

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

Syntax hints:   → wi 4   ∈ wcel 2143  Mndcmnd 18793  CMndccmn 19851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-cmn 19853

This theorem is referenced by:  pwsgprod  20412  psrbagev1  22209  evlslem1  22214  evlsvvval  22225  selvvvval  22274  psdadd  22307  evls1fpws  22510  mdetrsca  22741  cmn246135  33334  cmn145236  33335  gsummptres2  33354  gsummptfzsplitra  33359  gsummptfzsplitla  33360  gsumfs2d  33362  gsumtp  33365  gsumhashmul  33368  gsumwun  33377  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnsubrunlem1  33548  elrgspnsubrunlem2  33549  elrspunidl  33717  elrspunsn  33718  rprmdvdsprod  33805  dfufd2lem  33820  evlextv  33913  esplyfvaln  33945  vietalem  33950  fldextrspunlsplem  34044  fldextrspunlsp  34045  extdgfialglem2  34064  isprimroot2  42842  primrootsunit1  42845  primrootscoprmpow  42847  primrootscoprbij  42850  aks6d1c1p3  42858  aks6d1c1p4  42859  aks6d1c1p5  42860  aks6d1c1p7  42861  aks6d1c1p6  42862  aks6d1c1  42864  aks6d1c2lem4  42875  aks6d1c5lem0  42883  aks6d1c5lem2  42886  aks6d1c5  42887  aks5lem3a  42937  unitscyglem5  42947