Theorem con1bid

A contraposition deduction. (Contributed by NM, 9-Oct-1999.)

Hypothesis
con1bid.1
\( \vdash \varphi \rightarrow (\neg \psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\neg \chi \leftrightarrow \psi) \)
Proof
con1bid.1
bicomd _
con2bid _
bicomd _