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	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		tgptmd	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
2		tmdtps	⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp )
3	1 2	syl	⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )