= Solution
Both sequents follow directly from the introduction and elimination rules of the <implication-free fragment of intuitionistic propositional logic>. From a proof of $\phi\wedge(\psi\vee\chi)$, eliminate the conjunction to obtain $\phi$ and $\psi\vee\chi$. Eliminate the disjunction: in the $\psi$ branch introduce $\phi\wedge\psi$ and then the left disjunct; in the $\chi$ branch introduce $\phi\wedge\chi$ and then the right disjunct. This yields
$$
\phi\wedge(\psi\vee\chi)
\vdash
(\phi\wedge\psi)\vee(\phi\wedge\chi).
$$
Conversely, eliminate the outer disjunction. From $\phi\wedge\psi$, obtain $\phi$ and introduce the left side of $\psi\vee\chi$; from $\phi\wedge\chi$, obtain $\phi$ and introduce its right side. In either branch, conjunction introduction produces $\phi\wedge(\psi\vee\chi)$. Hence
$$
(\phi\wedge\psi)\vee(\phi\wedge\chi)
\vdash
\phi\wedge(\psi\vee\chi).
$$
This is the proof-theoretic form of the <distributive law for lattices>.
Back to article page
