Theorem lmodcmn

Description: A left module is a commutative monoid under addition. (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Assertion	lmodcmn	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
2		ablcmn	⊢ ( 𝑊 ∈ Abel → 𝑊 ∈ CMnd )
3	1 2	syl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )