Theorem pm2.8

Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Conclusion
\( \vdash \varphi \vee \psi \rightarrow \neg \psi \vee \chi \rightarrow \varphi \vee \chi \)
Proof
pm2.53
con1d _
orim1d _