Theorem con2bid

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

Hypothesis
con2bid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \neg \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \neg \psi) \)
Proof
l0
con2bid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \neg \chi) \)
con2bi
\( \vdash \chi \leftrightarrow \neg \psi \leftrightarrow (\psi \leftrightarrow \neg \chi) \)
sylibr l0 _