This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hmphsymb

Description: "Is homeomorphic to" is symmetric. (Contributed by FL, 22-Feb-2007)

		Ref	Expression
	Assertion	hmphsymb	$⊢ J ≃ K \leftrightarrow K ≃ J$

Step	Hyp	Ref	Expression
1		hmphsym	$⊢ J ≃ K \to K ≃ J$
2		hmphsym	$⊢ K ≃ J \to J ≃ K$
3	1 2	impbii	$⊢ J ≃ K \leftrightarrow K ≃ J$