Metamath Proof Explorer

Theorem bisym1

Description: A symmetry with <-> .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

Ref Expression
Assertion bisym1 ⊢ ψ ↔ ψ ↔ ⊥ → ψ ↔ φ

Proof

Step Hyp Ref Expression
1 nbfal ⊢ ¬ ψ ↔ ψ ↔ ⊥
2 1 bibi2i ⊢ ψ ↔ ¬ ψ ↔ ψ ↔ ψ ↔ ⊥
3 pm5.19 ⊢ ¬ ψ ↔ ¬ ψ
4 3 pm2.21i ⊢ ψ ↔ ¬ ψ → ψ ↔ φ
5 2 4 sylbir ⊢ ψ ↔ ψ ↔ ⊥ → ψ ↔ φ