Theorem con2bid

Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995)

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

Proof

Step	Hyp	Ref	Expression
1		con2bid.1	$$⊢\phi \to \left(\psi \leftrightarrow \neg \chi \right)$$
2		con2bi	$$⊢\left(\chi \leftrightarrow \neg \psi \right)\leftrightarrow \left(\psi \leftrightarrow \neg \chi \right)$$
3	1 2	sylibr	$$⊢\phi \to \left(\chi \leftrightarrow \neg \psi \right)$$