Theorem bifald

Description: Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017)

	Ref	Expression
Hypothesis	bifald.1	⊢ ( 𝜑 → ¬ 𝜓 )
Assertion	bifald	⊢ ( 𝜑 → ( 𝜓 ↔ ⊥ ) )

Proof

Step	Hyp	Ref	Expression
1		bifald.1	⊢ ( 𝜑 → ¬ 𝜓 )
2		id	⊢ ( 𝜓 → 𝜓 )
3		falim	⊢ ( ⊥ → 𝜓 )
4	2 3	pm5.21ni	⊢ ( ¬ 𝜓 → ( 𝜓 ↔ ⊥ ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝜓 ↔ ⊥ ) )