Theorem cmnmnd

Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Assertion	cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
3	1 2	iscmn	⊢ ( 𝐺 ∈ CMnd ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
4	3	simplbi	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )