Theorem cmnmndd 20024

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Mndcmnd 18929  CMndccmn 20000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6547  df-ov 7424  df-cmn 20002

This theorem is used by:  pwsgprod  20565  psrbagev1  22392  evlslem1  22397  evlsvvval  22408  selvvvval  22457  psdadd  22490  evls1fpws  22693  mdetrsca  22924  cmn246135  33641  cmn145236  33642  gsummptres2  33661  gsummptfzsplitra  33666  gsummptfzsplitla  33667  gsumfs2d  33669  gsumtp  33672  gsumhashmul  33675  gsumwun  33684  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  elrspunidl  34025  elrspunsn  34026  rprmdvdsprod  34113  dfufd2lem  34128  evlextv  34221  esplyfvaln  34253  vietalem  34258  fldextrspunlsplem  34352  fldextrspunlsp  34353  extdgfialglem2  34372  isprimroot2  43238  primrootsunit1  43241  primrootscoprmpow  43243  primrootscoprbij  43246  aks6d1c1p3  43254  aks6d1c1p4  43255  aks6d1c1p5  43256  aks6d1c1p7  43257  aks6d1c1p6  43258  aks6d1c1  43260  aks6d1c2lem4  43271  aks6d1c5lem0  43279  aks6d1c5lem2  43282  aks6d1c5  43283  aks5lem3a  43333  unitscyglem5  43343