Disjunction elimination rule

From $A\vee B$ and two subproofs deriving the same conclusion $C$, one under an additional assumption $A$ and the other under an additional assumption $B$, infer $C$ and discharge those two case assumptions. Any other assumptions remain in force.

If each of $A$, $B$ and $C$ separately yields the same conclusion $K$, then $A\vee B\vee C$ yields $K$, with the three case assumptions discharged. For $(A\vee B)\vee C$, first eliminate the outer logical disjunction, using a nested applications of the disjunction elimination rule on the $A\vee B$ branch. For $A\vee (B\vee C)$, nest the second elimination in the other branch. Common surrounding assumptions remain open.