Metamath Proof Explorer


Theorem hmphsymb

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

Ref Expression
Assertion hmphsymb J K K J

Proof

Step Hyp Ref Expression
1 hmphsym J K K J
2 hmphsym K J J K
3 1 2 impbii J K K J