Disjunction elimination

In symbolic logic, a valid inference in a system of truth-functional rules. This rule relies on the truth definition of the disjunction: Since a disjunction can be true in three ways, the desired statement must be derived from the assumption of each side of a disjunction. The rule involves successive subproof sequences for the desired statement, after which the second subproof is discharged and the desired statement is inferred. (See also Disjunctive Syllogism and Proof by Cases.)