| wedge-elim | Given a sentence (at line m) that is a disjunction and another sentence (at line n) that is a denial of one of its disjuncts, conclude the other disjunct. |
| Annotation: m, n vE | |
| Assumption set: The union of the assumption sets at lines m and n. | |
| Comment: The order of m and n in the proof is irrelevant. | |
| Also known as: Modus Tollendo Ponens (MTP), Disjunctive Syllogism (DS). | |
| Examples. | |
| (a) | |
1 (1) P v Q A | |
2 (2) ~P A | |
1,2 (3) Q 1,2 vE | |
| (b) | |
1 (1) P v (Q→R) A | |
2 (2) ~(Q→R) A | |
1,2 (3) P 1,2 vE | |
| (c) | |
1 (1) P v ~R A | |
2 (2) R A | |
1,2 (3) P 1,2 vE |