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 ${\displaystyle P}$ implies a statement ${\displaystyle Q}$ and a statement ${\displaystyle R}$ also implies ${\displaystyle Q}$, then if either ${\displaystyle P}$ or ${\displaystyle R}$ is true, then ${\displaystyle Q}$ has to be true. 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.

Disjunction elimination

Type	Rule of inference
Field	Propositional calculus
Statement	If a statement ${\displaystyle P}$ implies a statement ${\displaystyle Q}$ and a statement ${\displaystyle R}$ also implies ${\displaystyle Q}$, then if either ${\displaystyle P}$ or ${\displaystyle R}$ is true, then ${\displaystyle Q}$ has to be true.
Symbolic statement	${\displaystyle {\frac {P\to Q,R\to Q,P\lor R}{\therefore Q}}}$

An example in English:

If I'm inside, I have my wallet on me.

If I'm outside, I have my wallet on me.

It is true that either I'm inside or I'm outside.

Therefore, I have my wallet on me.

It is the rule can be stated as:

${\displaystyle {\frac {P\to Q,R\to Q,P\lor R}{\therefore Q}}}$

where the rule is that whenever instances of "${\displaystyle P\to Q}$", and "${\displaystyle R\to Q}$" and "${\displaystyle P\lor R}$" appear on lines of a proof, "${\displaystyle Q}$" can be placed on a subsequent line.