Theorem orddi

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

Conclusion
\( \vdash \varphi \wedge \psi \vee \chi \wedge \theta \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \vee \theta) \wedge ((\psi \vee \chi) \wedge (\psi \vee \theta)) \)
Proof
l0
ordir
\( \vdash \varphi \wedge \psi \vee \chi \wedge \theta \leftrightarrow (\varphi \vee \chi \wedge \theta) \wedge (\psi \vee \chi \wedge \theta) \)
l1
ordi
ordi
anbi12i l1 _
\( \vdash (\varphi \vee \chi \wedge \theta) \wedge (\psi \vee \chi \wedge \theta) \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \vee \theta) \wedge ((\psi \vee \chi) \wedge (\psi \vee \theta)) \)
bitri l0 _