$p \to (q\vee\neg r), \neg q, r ⊢ \neg p$ - Natural deduction- elimination with $\neg$ operator

Question

I have the following proposition:

$$p \to (q\vee\neg r), \neg q, r ⊢ \neg p$$

The only part I have trouble with is the :

$$p \to (q\vee\neg r)$$

Clearly the first step is to eliminate $q$ or $\neg r$ within the brackets, but I am not sure how to do that. The following elimination formula :

$$\varphi \wedge \psi/ \psi$$ $$\varphi \wedge\psi/\varphi$$

Can only be applied when both $\varphi$ and $\psi$ are true. However in the example above, only $p$ is true while $r$ is negated. So then how do I solve this?

Answer 1

"p→(q∨¬r)

Clearly the first step is to eliminate q or ¬r within the brackets"

I wouldn't do things this way. I'd assume (q∨¬r). Then since we have ¬q we can get to ¬r. But since we have r also, we have a contradiction, implying that (q∨¬r) is false giving us ¬(q∨¬r). Then since we have [p→(q∨¬r)] we can get to ¬p fairly easy.