Theorem simprim

Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)

Conclusion
\( \vdash \neg (\varphi \rightarrow \neg \psi) \rightarrow \psi \)
Proof
idd
impi _