= Three-case disjunction elimination
{title2=$A\lor B\lor C\vdash K$}
If each of $A$, $B$ and $C$ separately yields the same conclusion $K$, then $A\lor B\lor C$ yields $K$, with the three case assumptions discharged. For $(A\lor B)\lor C$, first eliminate the outer <logical disjunction>, using a nested applications of the <disjunction elimination rule> on the $A\lor B$ branch. For $A\lor(B\lor C)$, nest the second elimination in the other branch. Common surrounding assumptions remain open.
Back to article page
