I'm currently reading The Logic of Provability by George Boolos and there's a step in a proof that I don't understand.
The author has defined a system of modal logic called GL; its language has a countable collection of sentence letters $p$, $q$, $\ldots$ as well as the symbols $\to$, $\bot$ and $\Box$; sentences are defined inductively in the obvious way (i.e. $\bot$ and each sentence letter $p$ is a sentence, $(A \to B)$ and $\Box A$ are sentences whenever $A$ and $B$ are), $\neg A$ is defined to be $(A \to \bot)$ and $\Diamond A$ is defined to be $\neg \Box \neg A$.
The axioms of GL are all tautologies (although the author hasn't said as much, I assume that the truth of $\Box A$ should be taken as independent of that of any subsentences of $A$ in determining whether something is a tautology) as well as all sentences of the following forms:
$\Box (A \to B) \to (\Box A \to \Box B)$
$\Box (\Box A \to A) \to \Box A $
and its rules of inference are modus ponens and necessitation (i.e. from $A$ infer $\Box A$). It has been proved that all sentences of the form
$\Box A \to \Box \Box A$
are theorems, and that theorems of GL are closed under substitution of arbitrary sentences for sentence letters. The author has also proved Theorem 21 for all $p$:
$\mathrm{GL} \vdash \Box \bot \leftrightarrow \Box \Diamond p$.
A couple of pages later, the author says "by Theorem 21 (with $\bot$ for $p$)
$\mathrm{GL} \vdash \Box (p \leftrightarrow \neg \Box \bot) \to \Box \Box (p \leftrightarrow \neg \Box p)$"
I've been scratching my head for a while and I've no idea how he gets this. Can anyone help?