Theorem pm2.21

From a wff and its negation, anything follows. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its commuted form is pm2.24 and its associated inference is pm2.21i. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)

Conclusion
\( \vdash \neg \varphi \rightarrow \varphi \rightarrow \psi \)
Proof
id
pm2.21d _