Theorem pnrmtop

Description: A perfectly normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	pnrmtop	⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		pnrmnrm	⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Nrm )
2		nrmtop	⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
3	1 2	syl	⊢ ( 𝐽 ∈ PNrm → 𝐽 ∈ Top )