Theorem pm2.81

Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash (\psi \rightarrow \chi \rightarrow \theta) \rightarrow \varphi \vee \psi \rightarrow \varphi \vee \chi \rightarrow \varphi \vee \theta \)
Proof
l0
orim2
\( \vdash (\psi \rightarrow \chi \rightarrow \theta) \rightarrow \varphi \vee \psi \rightarrow \varphi \vee (\chi \rightarrow \theta) \)
pm2.76
\( \vdash \varphi \vee (\chi \rightarrow \theta) \rightarrow \varphi \vee \chi \rightarrow \varphi \vee \theta \)
syl6 l0 _