Prove $(\Box(p\supset q)\land\Diamond(p\land r))\supset\Diamond(q\land r)$ in K

Question

$(\Box(p\supset q)\land\Diamond(p\land r))\supset\Diamond(q\land r)$

Here's what I have so far:

1. $((p\supset q)\land(p\land r))\supset(q\land r)$, PC-valid WFF
2. $\Box(((p\supset q)\land(p\land r))\supset(q\land r))$, N (1)
3. $\Box((p\supset q)\land(p\land r))\supset\Box(q\land r)$, K (2)
4. $\Box((p\supset q)\land(p\land r))\equiv(\Box(p\supset q)\land\Box(p\land r))$, K3 instance
5. $(\Box(p\supset q)\land\Box(p\land r))\supset\Box(q\land r)$, Equiv (3),(4)

But now I'm stuck. This is problem 2.1c from Hughes and Cresswell. I think some instance of what they call K7 could be used:

$\Diamond(p\supset q)\equiv(\Box p\supset \Diamond q)$

Something like this:

$\Diamond(((p\supset q)\land(p\land r))\supset(q\land r))\equiv(\Box((p\supset q)\land(p\land r))\supset\Diamond(q\land r))$

But I don't know how to prove $\Diamond(((p\supset q)\land(p\land r))\supset(q\land r))$.

Thanks so much for any and all help.

Answer 1

$\def\pra#1{\left(#1\right)}$

Hint: apply K$\Diamond$ and MP on step 2, instead of K, next try to find where you can apply K7, the K$\Diamond$ is \begin{align} &\square\pra{\varphi\supset\psi}\supset\pra{\Diamond\varphi\supset\Diamond\psi}\tag{K$\Diamond$}\\ 1.&~~(\varphi\supset\psi)\supset(\lnot\psi\supset\lnot\varphi)\tag*{PC}\\ 2.&~~\square(\varphi\supset\psi)\supset\square(\lnot\psi\supset\lnot\varphi)\tag*{N,K,MP(1)}\\ 3.&~~\square(\lnot\psi\supset\lnot\varphi)\supset(\square\lnot\psi\supset\square\lnot\varphi)\tag*{K}\\ 4.&~~\square(\varphi\supset\psi)\supset(\square\lnot\psi\supset\square\lnot\varphi)\tag*{PC (2,3)}\\ 5.&~~\square(\varphi\supset\psi)\supset(\lnot\square\lnot\varphi\supset\lnot\square\lnot\psi)\tag*{PC(4)} \end{align}

If you got this right, your final proof might end up with something like the following \begin{align*} &~~\square(p\supset q)\land\Diamond(p\land r)\supset\Diamond(q\land r)\\ 1.&~~(p\supset q)\land(p\land r)\supset(q\land r)\tag*{PC}\\ 2.&~~\square((p\supset q)\land(p\land r)\supset(q\land r))\tag*{N(1)}\\ 3.&~~\Diamond((p\supset q)\land(p\land r))\supset\Diamond(q\land r)\tag*{K$\Diamond$,MP(2)}\\ 4.&~~\square(p\supset q)\land\Diamond(p\land r)\supset\Diamond((p\supset q)\land(p\land r))\tag*{K7,PC,MP}\\ 5.&~~\square(p\supset q)\land\Diamond(p\land r)\supset\Diamond(q\land r)\tag*{PC,MP(3,4)} \end{align*}