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