Theorem andi

Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Conclusion
\( \vdash \varphi \wedge (\psi \vee \chi) \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \chi \)
Proof
l0
orc
olc
l2
jaodan l0 _
orc
l4
anim2i _
olc
anim2i _
jaoi l4 _
impbii l2 _