Disjunction elimination rule
= Disjunction elimination rule
From $A\lor 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.