Theorem pm2.24

Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i. Commuted form of pm2.21. (Contributed by NM, 3-Jan-2005.)

Conclusion

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

Proof

pm2.21

com12 _