Theorem impcon4bid

A variation on impbid with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)

Hypotheses
impcon4bid.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
impcon4bid.2
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
impcon4bid.1
impcon4bid.2
con4d _
impbid l0 _