By S5, I mean the system consisting of the following axioms:
K: □(φ→ψ) → (□φ→□ψ)
T: □φ → φ
5: ◇φ → □◇φ
I believe the result I want to prove follows from K alone, but I cannot figure out how. If anyone can offer an explanation I would greatly appreciate it.
In the link you posted in the comments, it is claimed that $$\square (\forall x \square \varphi \rightarrow \square \varphi)\rightarrow (\lozenge \forall x \square \varphi \rightarrow \lozenge \square \varphi)$$ is a theorem of S5 modal propositional logic. Well, that's not exactly right, because this is not a propositional sentence (as indicated by the presence of the quantifier $\forall x$). What is meant is that this sentence is a substitution instance of the propositional theorem $$(\star)\quad\square (P \rightarrow Q) \rightarrow (\lozenge P \rightarrow \lozenge Q)$$ with $\forall x\square \varphi$ substituted for $P$ and $\square \varphi$ substituted for $Q$ in $(\star)$.
Now it should be intuitively clear that $(\star)$ is already a theorem of the modal logic K, since it is valid on every Kripke frame. Suppose we're at a world $w$ at which $\square (P\rightarrow Q)$ is true. If $\lozenge P$ is true, then $P$ holds at a world $w'$ accessible from $w$. But then $(P\rightarrow Q)$ holds at $w'$, so $Q$ holds at $w'$, so $\lozenge Q$ holds at $w$.
Ok, that was a semantic proof of $(\star)$ on Kripke frames. How would you give a formal proof? I'll give a sketch. Rewriting $\lozenge$ as $\lnot \square \lnot$, we want to prove $$(\star')\quad\square (P \rightarrow Q) \rightarrow (\lnot \square \lnot P \rightarrow \lnot \square \lnot Q).$$ By propositional logic, $(P\rightarrow Q)\rightarrow (\lnot Q\rightarrow \lnot P)$, so by necessitation and K, $\square(P\rightarrow Q)\rightarrow \square(\lnot Q\rightarrow \lnot P)$. Now if we assume $\square(P\rightarrow Q)$, by Modus Ponens we get $\square(\lnot Q\rightarrow \lnot P)$, so by K again, $\square \lnot Q \rightarrow \square \lnot P$. Taking the contrapositive again gives $\lnot \square \lnot P \rightarrow \lnot \square \lnot Q$, as desired.