Theorem cmnmndd 20011

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Mndcmnd 18916  CMndccmn 19987

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-cmn 19989

This theorem is used by:  pwsgprod  20552  psrbagev1  22379  evlslem1  22384  evlsvvval  22395  selvvvval  22444  psdadd  22477  evls1fpws  22680  mdetrsca  22911  cmn246135  33587  cmn145236  33588  gsummptres2  33607  gsummptfzsplitra  33612  gsummptfzsplitla  33613  gsumfs2d  33615  gsumtp  33618  gsumhashmul  33621  gsumwun  33630  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  elrspunidl  33971  elrspunsn  33972  rprmdvdsprod  34059  dfufd2lem  34074  evlextv  34167  esplyfvaln  34199  vietalem  34204  fldextrspunlsplem  34298  fldextrspunlsp  34299  extdgfialglem2  34318  isprimroot2  43124  primrootsunit1  43127  primrootscoprmpow  43129  primrootscoprbij  43132  aks6d1c1p3  43140  aks6d1c1p4  43141  aks6d1c1p5  43142  aks6d1c1p7  43143  aks6d1c1p6  43144  aks6d1c1  43146  aks6d1c2lem4  43157  aks6d1c5lem0  43165  aks6d1c5lem2  43168  aks6d1c5  43169  aks5lem3a  43219  unitscyglem5  43229