Disjunction elimination. This formalizes the proof by cases. If C follows in case of A as well as in case of B, then it follows from the disjunction A ∨ B too. Namely, if this disjunction, read "A or B", is true, then at least one of the propositions A, B should be true. But if the truth of C follows, regardless of which of them it is, then C stays constantly true under the truth of the disjunction. Therefore this rule must be valid.