Metamath Proof Explorer

Theorem tlmtps

Description: A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion tlmtps 
|- ( W e. TopMod -> W e. TopSp )

Proof

Step Hyp Ref Expression
1 tlmtmd 
 |-  ( W e. TopMod -> W e. TopMnd )
2 tmdtps 
 |-  ( W e. TopMnd -> W e. TopSp )
3 1 2 syl 
 |-  ( W e. TopMod -> W e. TopSp )