Theorem pm2.85

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

Conclusion

\( \vdash (\varphi \vee \psi \rightarrow \varphi \vee \chi) \rightarrow \varphi \vee (\psi \rightarrow \chi) \)

Proof

orimdi

biimpri _