Theorem con4bid

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

Hypothesis
con4bid.1
\( \vdash \varphi \rightarrow (\neg \psi \leftrightarrow \neg \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
con4bid.1
biimprd _
l2
con4d _
con4bid.1
biimpd _
impcon4bid l2 _