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