= Solution
Split on the <law of excluded middle> for $A$, then use <disjunction elimination>:
``
1 D ∧ E premise
2 (A ∧ D) → B premise
3 (¬A ∧ E) → B premise
4 D ∧-elim-L 1
5 E ∧-elim-R 1
6 A ∨ ¬A excluded middle
7 | A assumption
8 | A ∧ D ∧-intro 7,4
9 | B →-elim 2,8
10 | ¬A assumption
11 | ¬A ∧ E ∧-intro 10,5
12 | B →-elim 3,11
13 B ∨-elim 6,7–9,10–12
``
The two occurrences of $B$ have identical type and depend only on the corresponding temporary branch assumption and the original premises.
Back to article page
