Theorem
con2b
Contraposition. Bidirectional version of
con2
. (Contributed by NM, 12-Mar-1993.)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \psi \rightarrow \neg \varphi \)
Proof
l0
con2
con2
impbii
l0
_
This is the content in the right pane.