Metamath Proof Explorer

Theorem clmabl

Description: A subcomplex module is an abelian group. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Assertion clmabl ⊢ W ∈ CMod → W ∈ Abel

Proof

Step Hyp Ref Expression
1 clmlmod ⊢ W ∈ CMod → W ∈ LMod
2 lmodabl ⊢ W ∈ LMod → W ∈ Abel
3 1 2 syl ⊢ W ∈ CMod → W ∈ Abel