Theorem anddi

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

Conclusion
\( \vdash (\varphi \vee \psi) \wedge (\chi \vee \theta) \leftrightarrow \varphi \wedge \chi \vee \varphi \wedge \theta \vee (\psi \wedge \chi \vee \psi \wedge \theta) \)
Proof
l0
andir
\( \vdash (\varphi \vee \psi) \wedge (\chi \vee \theta) \leftrightarrow \varphi \wedge (\chi \vee \theta) \vee \psi \wedge (\chi \vee \theta) \)
l1
andi
andi
orbi12i l1 _
\( \vdash \varphi \wedge (\chi \vee \theta) \vee \psi \wedge (\chi \vee \theta) \leftrightarrow \varphi \wedge \chi \vee \varphi \wedge \theta \vee (\psi \wedge \chi \vee \psi \wedge \theta) \)
bitri l0 _