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:
α ∨ β, ¬β α