Theorem orel2

Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)

Conclusion
\( \vdash \neg \varphi \rightarrow \psi \vee \varphi \rightarrow \psi \)
Proof
l0
idd
pm2.21
jaod l0 _