Theorem iman

Implication in terms of conjunction and negation. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow \neg (\varphi \wedge \neg \psi) \)
Proof
notnotb
l1
imbi2i _
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \neg \neg \psi \)
imnan
\( \vdash \varphi \rightarrow \neg \neg \psi \leftrightarrow \neg (\varphi \wedge \neg \psi) \)
bitri l1 _