Metamath Proof Explorer

Theorem slmdmnd

Description: A semimodule is a monoid. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion slmdmnd ⊢ W ∈ SLMod → W ∈ Mnd

Proof

Step Hyp Ref Expression
1 slmdcmn ⊢ W ∈ SLMod → W ∈ CMnd
2 cmnmnd ⊢ W ∈ CMnd → W ∈ Mnd
3 1 2 syl ⊢ W ∈ SLMod → W ∈ Mnd