How to prove Hilbert-style $(\Box(p\rightarrow q)\wedge\Diamond(p\wedge r))\rightarrow\Diamond(q\wedge r)$ in **K**?

Question

Edit: I figured out how to solve it using the theorem K9: $\Box(p\vee q)\rightarrow\Box p\vee\Diamond q$ on p. 36 and then manipulating it using the rules of propositional logic. If you have any alternative suggestions, feel free to respond.

I am trying to solve (c) of Exercise 2.1 (p. 48) in Hughes and Cresswell's New Introduction to Modal Logic. Here is what I attempted (in $\LaTeX$ notation):

1. $\Box(p\rightarrow q)\rightarrow\Box((p\rightarrow r)\rightarrow(p\rightarrow(q\wedge r)))$ (valid in K)

2. $\Box(p\rightarrow q)\rightarrow(\Diamond(p\rightarrow r)\rightarrow\Diamond(p\rightarrow(q\wedge r)))$

3. $\neg\Box(p\rightarrow q)\vee(\Diamond(p\rightarrow r)\rightarrow\Diamond(p\rightarrow(q\wedge r)))$

4. $\neg(\Box(p\rightarrow q)\wedge\Diamond(\neg p\vee r))\vee\Diamond(\neg p\vee(q\wedge r))$

5. $\ldots$

6. $\ldots$

7. $\ldots$

8. $(\Box(p\rightarrow q)\wedge\Diamond\neg(p\wedge\neg r))\rightarrow\Diamond(\neg(p\wedge\neg(q\wedge r)))$

Answer 1

I’ll set you up with the “boxed” instance of the propositional theorem you’ll want to use to prove this. You’ll also have to use the equivalence

$(p \to (q \to r)) \leftrightarrow ((p \land q) \to r)$.

Here’s how I would get started:

1. $\Box ((p \to q) \to ((p \land r) \to (q \land r)))$