Metamath Proof Explorer


Theorem lmodcmn

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

Ref Expression
Assertion lmodcmn W LMod W CMnd

Proof

Step Hyp Ref Expression
1 lmodabl W LMod W Abel
2 ablcmn W Abel W CMnd
3 1 2 syl W LMod W CMnd