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.
 A: 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$
A: I know you already have the answer you need, and you can't use this proof anyway since it uses an assumption, but it's kind of cute and I feel like it might be nice to provide a complete non-constructive proof. Feel free to ignore this if you'd like, I'm just throwing this in for fun.
Again continuing where you left off, assume $\neg r.$ By Modus Ponens, we have $p \vee \neg q.$
By conjunction with $(1)$, we now have $(p \vee \neg q) \wedge (p \vee q),$ which we can expand to $(p \vee \neg q \wedge p) \vee (p \vee q \wedge \neg q),$ and then $(p \wedge  p) \vee (q \wedge p) \vee (p \wedge \neg q) \vee (q \wedge \neg q)$ by the distributive property. $p \wedge p$ simplifies to $p$ and $q \wedge \neg q$ simplifies to false, so we get $p \vee (p \wedge q) \vee (p \wedge \neg q).$
Now using the distributive property in reverse gives us $p \vee (p \wedge (q \vee \neg q)),$ which simplifies to $p \vee p$ and then just $p.$
We assumed $\neg r$ and we reached $p,$ so we can conclude that $\neg r \to p.$
Both the direct proof and the proof by contradiction where we assume $\neg r$ and $p$ are admittedly simpler than this, but like I said I just felt like sharing it for fun.
A: 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.
