Theorem cmnmndd 19931

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Mndcmnd 18836  CMndccmn 19907

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7416  df-cmn 19909

This theorem is used by:  pwsgprod  20470  psrbagev1  22293  evlslem1  22298  evlsvvval  22309  selvvvval  22358  psdadd  22391  evls1fpws  22594  mdetrsca  22825  cmn246135  33473  cmn145236  33474  gsummptres2  33493  gsummptfzsplitra  33498  gsummptfzsplitla  33499  gsumfs2d  33501  gsumtp  33504  gsumhashmul  33507  gsumwun  33516  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  elrspunidl  33856  elrspunsn  33857  rprmdvdsprod  33944  dfufd2lem  33959  evlextv  34052  esplyfvaln  34084  vietalem  34089  fldextrspunlsplem  34183  fldextrspunlsp  34184  extdgfialglem2  34203  isprimroot2  42960  primrootsunit1  42963  primrootscoprmpow  42965  primrootscoprbij  42968  aks6d1c1p3  42976  aks6d1c1p4  42977  aks6d1c1p5  42978  aks6d1c1p7  42979  aks6d1c1p6  42980  aks6d1c1  42982  aks6d1c2lem4  42993  aks6d1c5lem0  43001  aks6d1c5lem2  43004  aks6d1c5  43005  aks5lem3a  43055  unitscyglem5  43065