Theorem slmdmnd

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

	Ref	Expression
Assertion	slmdmnd	⊢ ( 𝑊 ∈ SLMod → 𝑊 ∈ Mnd )

Proof

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