Name of an inference rule that I can't find anywhere As a homework question, I must prove, using inference rules, that:
p ∨ q
(¬p ∧ q) → r

∴ ¬r → p
I have done the following progress:

p ∨ q

(¬p ∧ q) → r

¬r → ¬(¬p ∧ q)

¬r → (¬(¬p) ∨ ¬q)

¬r → (p ∨ ¬q)


1 premisse
2 premisse
3 contrapositive from 2
4 morgan law from 3
5 double negation from 4
And I can't figure out how to finish it. I can easily prove the whole expression using a truth-table, but I simply can't find a formal way of merging 1 and 5. Any help would be hugely appreciated.
Here's a way to do this directly:
$p \to p,$ LEM as an implication
$\neg q \to p,$ $1$ as an implication
$(p \vee \neg q) \to (p \vee p),$ constructive syllogism
$(p \vee \neg q) \to p$
$\neg r \to p,$ hypothetical syllogism from the above and $5$
hint
You want to prove that $\lnot r \to p$.
you proved that $ \lnot r \to (p\vee \lnot q)$.
Assume  $ \lnot p$.
then by DS, $ \lnot q$.
but the first premise is $ p\vee q$
so, we can't have $ \lnot p \wedge \lnot q$. this is the contradiction.