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 ( ( 𝜓 ↔ ( 𝜓 ↔ ⊥ ) ) → ( 𝜓𝜑 ) )