Proving $\phi\wedge\Box\Box\phi\rightarrow\Box(\phi\wedge\Box\Box\phi)$ I want to know why the formula $\phi\wedge\Box\Box\phi\rightarrow\Box(\phi\wedge\Box\Box\phi)$ is provable in modal logic K5.
Because I think we need more axioms in order to prove the formula.
Also, why does $\phi\vdash_{K5}\phi\wedge\Box\Box\phi$
hold but $\phi\vdash\phi\wedge\Box\phi$
does not hold in K5?
 A: I don't have access to the paper you linked to in the comments, but I think I have a countermodel demonstrating the failure of the formula that you mentioned in K5.
So, I'm interpreting K5 as the modal logic whose accessibility relations are constrained to be Euclidean. This means that, if $aRb$ and $aRc$, then it holds that $bRc$ and $cRb$. The $cRb$ conclusion is implied by exchanging the roles of $a$ and $b$, but I like including it for symmetry. If $S$ is an arbitrary relation, let's call the result of adding in all the edges implied by the Euclidean property the Euclidean closure of $S$.
There's another important consequence of being a Euclidean relation pointed out by Alex Kruckman in the comments: if $aRb$, then it holds that $bRb$. In prose, any world of in-degree at least one is self-accessible. This is because the world is directly self-accessible, or the world is self-accessible by virtue of being a Euclidean relation, or both.
The original formula $\phi \land \square \square \phi \to \square(\phi \land \square \square \phi)$ is not a tautology in K5.
Here's how to prove it.
Let the set of worlds be $\{0, 1, 2, 3\}$. Suppose it holds that $0R1, 1R2, 2R3$ and also that $1R1, 2R2, 3R3$. The Euclidean closure of $R$ would add no edges, thus $R$ is Euclidean
Suppose that $A$ holds at $0, 1, 2$ but fails at $3$.
Let's evaluate the truth of the above formula at world $0$ and let $\phi$ be $A$.
Since $A$ holds at $0$ and $2$, $A$ and $\square \square A$ are both true at $0$.
However, $A$ fails at $3$, so at least one of $\{A, \square \square A\}$ fails at $1$.
Thus $\phi \land \square \square \phi \to \square(\phi \land \square \square \phi)$ fails at $0$.
