Disjunction property of intuitionistic propositional logic (source code)

= Disjunction property of intuitionistic propositional logic
{wiki=Disjunction_property}

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