Prove P from B ∨ P when we have proven ¬B

Question

I have the following proof so far:

In step 9 I'm not sure how to prove P from the steps I have before. I thought that I could use ∨ Elim but I don't think I can now.

Answer 1

The trick is to use $\bot \ Elim$. Now, to continue from what you have, you can do:

But note that you never used the subproof on lines 5-7, so this can be simplified to:

Although conceptually, it may be helpful to keep the original subproof, and (since it shows that $B$ leads to a contradiction $\bot$) derive $\neg B$, and to then combine $\neg B$ with $B \lor P$ (the latter is a super common patterns, so remember that one!!):

Finally, you can set this up as a proof by cases within a conditional proof, i.e. derive your goal $P \land D$ from each of the cases $B$ and $P$:

Answer 2

I've actually seen some texts define Or-Elimination as $$\frac{\lnot B,~ B \lor P}{P}$$ which is actually constructively valid. Anyway, the way to get there from regular Or-Elimination (proof by cases) is just to show that in both cases of $B$ and case $P$ that $P$ follows:

$$\begin{array} {rll} (1) & \lnot B & \text{Given} \\ \\ % (2) & \quad B & \text{assumption, Case 1} \\ % (3) & \quad \bot & \text{Contradiction} \\ % (4) & \quad P & \text{Explosion} \\ \\ % (5) & \quad P & \text{assumption, Case 2} \\ \\ % (6) & B \lor P & \text{Given} \\ % (7) & P & \text{Proof by cases (Or Elim) of 6, 2 through 4, 5 through 5} \\ % \end{array}$$