Theorem orel1

Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)

Conclusion
\( \vdash \neg \varphi \rightarrow \varphi \vee \psi \rightarrow \psi \)
Proof
pm2.53
com12 _