Theorem
pm2.36
Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
Conclusion
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \vee \psi \rightarrow \chi \vee \varphi \)
Proof
l0
pm1.4
\( \vdash \varphi \vee \psi \rightarrow \psi \vee \varphi \)
pm2.38
\( \vdash (\psi \rightarrow \chi) \rightarrow \psi \vee \varphi \rightarrow \chi \vee \varphi \)
syl5
l0
_
This is the content in the right pane.