Theorem andir

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

Conclusion
\( \vdash (\varphi \vee \psi) \wedge \chi \leftrightarrow \varphi \wedge \chi \vee \psi \wedge \chi \)
Proof
l0
andi
\( \vdash \chi \wedge (\varphi \vee \psi) \leftrightarrow \chi \wedge \varphi \vee \chi \wedge \psi \)
l1
ancom
\( \vdash (\varphi \vee \psi) \wedge \chi \leftrightarrow \chi \wedge (\varphi \vee \psi) \)
l2
ancom
ancom
orbi12i l2 _
\( \vdash \varphi \wedge \chi \vee \psi \wedge \chi \leftrightarrow \chi \wedge \varphi \vee \chi \wedge \psi \)
3bitr4i l0 l1 _