Theorem pm2.26

Theorem *2.26 of [WhiteheadRussell] p. 104. See pm2.27. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

Conclusion
\( \vdash \neg \varphi \vee ((\varphi \rightarrow \psi) \rightarrow \psi) \)
Proof
pm2.27
imori _