Help with modal logical deduction in K4 The following deduction can be found from the Boolos - The Logic of Provability in the page 59. It is in the proof for arithmetical soundness theorem.
Let's assign 
\begin{align*}
&B = \square ( \square A \rightarrow A)\\
&C = \square A\\
&D = B \rightarrow C = \square ( \square A \rightarrow A) \rightarrow \square A
\end{align*}
Then
\begin{align*}
K4 &\vdash \square (B \rightarrow C) \rightarrow (\square B \rightarrow \square C) &&\text{Distribution axiom}\\
K4 &\vdash B \rightarrow (\square C \rightarrow C) && \text{Distribution axiom}\\
K4  &\vdash B \rightarrow \square B && \text{transitivity / 4}\\
K4 &\vdash \square (B \rightarrow  C) \rightarrow (B \rightarrow C) && \text{???}\\
\end{align*}
I know the last line should be a tautological consequence of the three lines above. I suppose it's something pretty straight forward, but I just don't get it. Thank you for helping.
 A: Let us show that $\square D \rightarrow D$ follows truth-functionally from (and so is a tautological consequence of) the three formulae above it.
From the hypotheses $H_1 =\square D \rightarrow (\square B \rightarrow \square C), H_2 = B \rightarrow (\square C \rightarrow C), H_3 = B \rightarrow \square B\ $ we need to deduce $\square D \rightarrow D$.
So from $H_1, H_2, H_3$ and $\square D$ we need to deduce $D$, that is $B \rightarrow C$. 
Hence from $H_1, H_2, H_3, \square D$ and $B$ we need to deduce $C$. 
From $H_1$ and $\square D$ we get $\square B \rightarrow \square C$. From $H_3$ and $B$ we get $\square B$. From $\square B$ and $\square B \rightarrow \square C$ we get $\square C$. Now, from $H_2$ and $B$ we get $\square C \rightarrow C$. Finally, from $\square C$ and $\square C \rightarrow C$ we get $C$.
The above shows that whenver all $H_1, H_2, H_3$ are true, so is $\square D \rightarrow D$, hence by the completeness theorem for propositional calculus $\square D \rightarrow D$ is a tautological consequence of these hypotheses. Also if you need  an actual proof in propositional calculus, the argument above can be transformed into such a proof by appealing to the deduction theorem.
