Theorem cmnmndd 19770

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

Syntax hints:   → wi 4   ∈ wcel 2119  Mndcmnd 18693  CMndccmn 19746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-cmn 19748

This theorem is referenced by:  pwsgprod  20300  psrbagev1  22053  evlslem1  22058  evlsvvval  22069  selvvvval  22118  psdadd  22151  evls1fpws  22355  mdetrsca  22586  cmn246135  33112  cmn145236  33113  gsummptres2  33134  gsummptfzsplitra  33139  gsummptfzsplitla  33140  gsumfs2d  33142  gsumtp  33145  gsumhashmul  33148  gsumwun  33157  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  elrspunidl  33511  elrspunsn  33512  rprmdvdsprod  33617  dfufd2lem  33632  evlextv  33726  esplyfvaln  33758  vietalem  33763  fldextrspunlsplem  33857  fldextrspunlsp  33858  extdgfialglem2  33877  isprimroot2  42579  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p7  42598  aks6d1c1p6  42599  aks6d1c1  42601  aks6d1c2lem4  42612  aks6d1c5lem0  42620  aks6d1c5lem2  42623  aks6d1c5  42624  aks5lem3a  42674  unitscyglem5  42684