Proof of $p\rightarrow (\Box (\Box p \wedge p) \rightarrow (\Box p \wedge p))$

Question

I need to prove:

$$p\rightarrow (\Box (\Box p \wedge p) \rightarrow (\Box p \wedge p))$$

The system contains all propostional tautologies and the axiom scheme $\mathbf K$:$ \Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q) $.

Rules are modus ponens, substitution and necessitation.

Thanks for help!

Answer 1

$\square p\land p\to p$ is a theorem; therefore $\square(\square p\land p\to p)$ by necessitation, and so $$ \square(\square p\land p)\to \square p $$ by $\mathbf K$ (and modus ponens). Now apply $p\land\cdot$ to both sides and use the equivalence of $a\land b\to c$ and $a\to(b\to c)$.