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 )