= Solution
Now derive the needed $D$ or $E$ inside its respective <subproof>:
``
1 A → D premise
2 ¬A → E premise
3 (A ∧ D) → B premise
4 (¬A ∧ E) → B premise
5 A ∨ ¬A excluded middle
6 | A assumption
7 | D →-elim 1,6
8 | A ∧ D ∧-intro 6,7
9 | B →-elim 3,8
10 | ¬A assumption
11 | E →-elim 2,10
12 | ¬A ∧ E ∧-intro 10,11
13 | B →-elim 4,12
14 B ∨-elim 5,6–9,10–13
``
<Implication elimination> supplies the branch-specific premise before <conjunction introduction> packages it for the final implication.
Back to article page
