In propositional logic, disjunction elimination[1][2] (sometimes named proof by cases, case analysis, or or elimination) is the valid argument form and rule of inference that allows one to eliminate a disjunctive statement from a logical proof.

It is the inference that if a statement

implies a statement

The reasoning is simple: since at least one of the statements P and R is true, and since either of them would be sufficient to entail Q, Q is certainly true.

An example in English: It is the rule can be stated as: where the rule is that whenever instances of "

" can be placed on a subsequent line.

The disjunction elimination rule may be written in sequent notation: where

is a metalogical symbol meaning that

in some logical system; and expressed as a truth-functional tautology or theorem of propositional logic: where

are propositions expressed in some formal system.