Theorem pm2.74

Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Conclusion
\( \vdash (\psi \rightarrow \varphi) \rightarrow \varphi \vee \psi \vee \chi \rightarrow \varphi \vee \chi \)
Proof
l0
orel2
ax-1
ja l0 _
orim1d _