Implication-free fragment of intuitionistic propositional logic ($\mathrm{IPC}\setminus \{\to \}$)

The implication-free fragment uses only conjunction, disjunction, truth, and falsity, with their intuitionistic natural-deduction rules.

An implication-free formula is provable exactly when every valuation into every bounded distributive lattice assigns it the top element.