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