Theorem pm2.521

Theorem *2.521 of [WhiteheadRussell] p. 107. Instance of pm2.521g and of pm2.521g2. (Contributed by NM, 3-Jan-2005.)

Conclusion

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

Proof

pm2.521g