Theorem ordir

Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)

Conclusion
\( \vdash \varphi \wedge \psi \vee \chi \leftrightarrow (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
Proof
l0
ordi
\( \vdash \chi \vee \varphi \wedge \psi \leftrightarrow (\chi \vee \varphi) \wedge (\chi \vee \psi) \)
l1
orcom
\( \vdash \varphi \wedge \psi \vee \chi \leftrightarrow \chi \vee \varphi \wedge \psi \)
l2
orcom
orcom
anbi12i l2 _
\( \vdash (\varphi \vee \chi) \wedge (\psi \vee \chi) \leftrightarrow (\chi \vee \varphi) \wedge (\chi \vee \psi) \)
3bitr4i l0 l1 _