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 e. LMod -> W e. CMnd )

Proof

Step Hyp Ref Expression
1 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
2 ablcmn 
 |-  ( W e. Abel -> W e. CMnd )
3 1 2 syl 
 |-  ( W e. LMod -> W e. CMnd )