Theorem pm2.1

Theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

Conclusion
\( \vdash \neg \varphi \vee \varphi \)
Proof
id
imori _