Theorem cmnmndd

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

	Ref	Expression
Hypothesis	cmnmndd.1	|- ( ph -> G e. CMnd )
Assertion	cmnmndd	|- ( ph -> G e. Mnd )

Proof

Step	Hyp	Ref	Expression
1		cmnmndd.1	|- ( ph -> G e. CMnd )
2		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
3	1 2	syl	|- ( ph -> G e. Mnd )