disjunction elimination
From A ∨ B and two subproofs reaching the same C, one from A and one from B, write C.
Disjunction elimination (∨E), or proof by cases, lets you write C when A ∨ B is available and there are two closed subproofs, one assuming A and reaching C, the other assuming B and reaching C.
Examples
From P ∨ Q, a subproof P … R, and a subproof Q … R, write R.
See also