Show premise implies conclusion using resolution

Question

I'm looking into rules of inference and in particular resolution, e.g.

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

Now in the textbook I see the following example but I don't quite understand it

Show that the premises (p ∧ q) ∨ r and r → s imply the conclusion p ∨ s.
And here are the steps from the textbook to show this:

1. Rewrite (p ∧ q) ∨ r as (p ∨ r) ∧ (q ∨ r)
2. Rewrite r → s by the equivalent clause ¬r ∨ s
3. Using the resolution we can conclude p ∨ s

Now I'm having a bit trouble understanding the above. To me the task is to show this:

$$((p ∧ q) ∨ r) ∧ (r → s) → p ∨ s$$

Now while I understand where first 2 steps come from, can't quite get my head around the 3rd one. After first 2 steps this is what we have (I think)

$$((p ∨ r) ∧ (q ∨ r)) ∧ (¬r ∨ s)$$

How it goes from here to conclude that

$$((p ∨ r) ∧ (q ∨ r)) ∧ (¬r ∨ s) → p ∨ s$$

is what I'm having hard time understanding.

I tried to use Commutativity, Associativity to go from

$$((p ∨ r) ∧ (q ∨ r)) ∧ (¬r ∨ s)$$

to

$$((r ∨ p) ∧ (¬r ∨ s)) ∧ (q ∨ r)$$

Here I see that the first part is a Resolution: $$((r ∨ p) ∧ (¬r ∨ s)) → (p ∨ s)$$

but can't understand what about: $$∧ (q ∨ r)$$

Answer 1

It's extra information we don't need. Since it's connect with an AND, we can discard it if necessary. Using conjunction elimination, we know from: $$ ((r ∨ p) ∧ (¬r ∨ s)) ∧ (q ∨ r) $$

we can infer that: $$ (r ∨ p) ∧ (¬r ∨ s) $$

and so by resolution, we conclude that $p \lor s$, as desired.