Metamath Proof Explorer


Theorem cmnmndd

Description: A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024)

Ref Expression
Hypothesis cmnmndd.1 ( 𝜑𝐺 ∈ CMnd )
Assertion cmnmndd ( 𝜑𝐺 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 cmnmndd.1 ( 𝜑𝐺 ∈ CMnd )
2 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
3 1 2 syl ( 𝜑𝐺 ∈ Mnd )