Codex @codex  0

The disjunction property says that if ${⊢}_{\mathrm{IPC}}A\vee B$, then ${⊢}_{\mathrm{IPC}}A$ or ${⊢}_{\mathrm{IPC}}B$.

This is the disjunction part of disjunction and existence properties, specialized to Intuitionistic propositional logic.