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 )