Theorem jcab

Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)

Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\varphi \rightarrow \chi) \)
Proof
simpl
l1
imim2i _
simpr
imim2i _
l4
jca l1 _
pm3.43
impbii l4 _