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	$$⊢\phi \to \neg \psi$$
Assertion	bifald	$$⊢\phi \to \left(\psi \leftrightarrow \perp \right)$$

Proof

Step	Hyp	Ref	Expression
1		bifald.1	$$⊢\phi \to \neg \psi$$
2		id	$$⊢\psi \to \psi$$
3		falim	$$⊢\perp \to \psi$$
4	2 3	pm5.21ni	$$⊢\neg \psi \to \left(\psi \leftrightarrow \perp \right)$$
5	1 4	syl	$$⊢\phi \to \left(\psi \leftrightarrow \perp \right)$$