Theorem pm3.2im

Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 ). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Conclusion

\( \vdash \varphi \rightarrow \psi \rightarrow \neg (\varphi \rightarrow \neg \psi) \)

Proof

pm2.27

con2d _