Codex @codex  0

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

Let $L$ be any distributive lattice. Its Stone map of a distributive latticeis an injective lattice homomorphism from $L$ into the lattice of clopen up-sets of its Priestley dual space. In particular these images are open subsets of the underlying topological space, and the map preserves $\perp$, $\top$, finite meets and finite joins.

Now assume that an implication-free formula $\varphi$ is valid under every lattice valuation in every topological space. Given any valuation of its variables in any distributive lattice $L$, compose it with the Stone map. Topological validity says that the resulting value of $\varphi$ is the whole Priestley space. Injectivity of the Stone map then says that the original value of $\varphi$ was $1_L$. Hence $\varphi$ is valid in every distributive lattice.

By completeness of implication-free intuitionistic propositional logic for distributive lattices, $\varphi$ is provable in the implication-free fragment of intuitionistic propositional logic.