Theorem pm4.78

Implication distributes over disjunction. Theorem *4.78 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \vee (\varphi \rightarrow \chi) \leftrightarrow \varphi \rightarrow \psi \vee \chi \)
Proof
l0
orordi
\( \vdash \neg \varphi \vee (\psi \vee \chi) \leftrightarrow \neg \varphi \vee \psi \vee (\neg \varphi \vee \chi) \)
l1
imor
\( \vdash \varphi \rightarrow \psi \vee \chi \leftrightarrow \neg \varphi \vee (\psi \vee \chi) \)
l2
imor
imor
orbi12i l2 _
\( \vdash (\varphi \rightarrow \psi) \vee (\varphi \rightarrow \chi) \leftrightarrow \neg \varphi \vee \psi \vee (\neg \varphi \vee \chi) \)
3bitr4ri l0 l1 _