The classical principle of proof by cases, Disjunction Elimination allows the inference of somthing that follows from both sides of a disjunction.
Preview shown for the Typed Forward Strict derivation type in the LRC system
