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