Theorem con4bid

Description: A contraposition deduction. (Contributed by NM, 21-May-1994)

	Ref	Expression
Hypothesis	con4bid.1	$$⊢\phi \to \left(\neg \psi \leftrightarrow \neg \chi \right)$$
Assertion	con4bid	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		con4bid.1	$$⊢\phi \to \left(\neg \psi \leftrightarrow \neg \chi \right)$$
2	1	biimprd	$$⊢\phi \to \left(\neg \chi \to \neg \psi \right)$$
3	2	con4d	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1	biimpd	$$⊢\phi \to \left(\neg \psi \to \neg \chi \right)$$
5	3 4	impcon4bid	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$