Metamath Proof Explorer

Theorem slmdmnd

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

Ref Expression
Assertion slmdmnd 
|- ( W e. SLMod -> W e. Mnd )

Proof

Step Hyp Ref Expression
1 slmdcmn 
 |-  ( W e. SLMod -> W e. CMnd )
2 cmnmnd 
 |-  ( W e. CMnd -> W e. Mnd )
3 1 2 syl 
 |-  ( W e. SLMod -> W e. Mnd )