Theorem lmodcmn

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

	Ref	Expression
Assertion	lmodcmn	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
2		ablcmn	$$⊢W\in \mathrm{Abel}\to W\in \mathrm{CMnd}$$
3	1 2	syl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{CMnd}$$