Theorem cmnmndd 19740

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18667  CMndccmn 19716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392  df-cmn 19718

This theorem is referenced by:  psrbagev1  21990  evlslem1  21995  psdadd  22056  evls1fpws  22262  mdetrsca  22496  cmn246135  32980  cmn145236  32981  gsummptres2  32999  gsumfs2d  33001  gsumtp  33004  gsumhashmul  33007  gsumwun  33011  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnsubrunlem1  33204  elrgspnsubrunlem2  33205  elrspunidl  33405  elrspunsn  33406  rprmdvdsprod  33511  dfufd2lem  33526  fldextrspunlsplem  33674  fldextrspunlsp  33675  isprimroot2  42077  primrootsunit1  42080  primrootscoprmpow  42082  primrootscoprbij  42085  aks6d1c1p3  42093  aks6d1c1p4  42094  aks6d1c1p5  42095  aks6d1c1p7  42096  aks6d1c1p6  42097  aks6d1c1  42099  aks6d1c2lem4  42110  aks6d1c5lem0  42118  aks6d1c5lem2  42121  aks6d1c5  42122  aks5lem3a  42172  unitscyglem5  42182  pwsgprod  42525  evlsvvval  42544  selvvvval  42566