Metamath Proof Explorer

Theorem tgptps

Description: A topological group is a topological space. (Contributed by FL, 21-Jun-2010) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion tgptps 
|- ( G e. TopGrp -> G e. TopSp )

Proof

Step Hyp Ref Expression
1 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
2 tmdtps 
 |-  ( G e. TopMnd -> G e. TopSp )
3 1 2 syl 
 |-  ( G e. TopGrp -> G e. TopSp )