If you have P ∨ Q, and both P → R and Q → R, then R.
This is the most complex rule so far — it has three premises. It formalises case analysis: when you know "P or Q" holds, you prove your goal R in each case separately. If R follows from P and R follows from Q, then R follows from P ∨ Q regardless of which disjunct is true.
[P]¹ [Q]²
⋮ ⋮
P ∨ Q R R
——————————————————— ∨-Elim¹⋅²
R
The two sub-derivations (from [P] to R and from [Q] to R) represent the two cases. Both assumptions are discharged by the rule.
| Prover | Syntax |
|---|---|
| Lean 4 | rcases h with hp | hq |
| Coq | destruct H as [HP | HQ] |
| Agda | pattern matching with two clauses |
See also: Logic §04 — Disjunction | Strategies §03 — Case analysis
Prove P ∨ Q → Q ∨ P (commutativity of disjunction).
Use →-Intro to assume P ∨ Q, then ∨-Elim to case-split. In the P case, use ∨-Intro&sub2; to get Q ∨ P. In the Q case, use ∨-Intro&sub1;.
[P]¹ [Q]²
——————— ∨-Intro&sub2; ——————— ∨-Intro&sub1;
[P ∨ Q]³ Q ∨ P Q ∨ P
——————————————————————————— ∨-Elim¹⋅²
Q ∨ P
————————————————————————————— →-Intro³
P ∨ Q → Q ∨ P
In the P case you inject right (∨-Intro&sub2;); in the Q case you inject left (∨-Intro&sub1;). Both cases yield Q ∨ P.