Theorem ordi

Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 28-Nov-2013.)

Conclusion
\( \vdash \varphi \vee \psi \wedge \chi \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \)
Proof
l0
jcab
\( \vdash \neg \varphi \rightarrow \psi \wedge \chi \leftrightarrow (\neg \varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
l1
df-or
\( \vdash \varphi \vee \psi \wedge \chi \leftrightarrow \neg \varphi \rightarrow \psi \wedge \chi \)
l2
df-or
df-or
anbi12i l2 _
\( \vdash (\varphi \vee \psi) \wedge (\varphi \vee \chi) \leftrightarrow (\neg \varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
3bitr4i l0 l1 _