**Separation of cases** is a basic rule of inference in logic by which a true proposition or formula is obtained from a disjunction when the alternative formula is known to be false. Separation of cases is also known as the **disjunction elimination** rule of inference (or ∨E), and explains that "P or Q, ¬P, therefore Q".

Separation of cases may be formally presented as follows:

**α ∨ β, ¬α β**

…and:

**α ∨ β, ¬β α**