Of monotone formulas and same ones satisfying certain properties
Spira's result uses the technique of formula balancing. For simplicity, I describe the non-monotone case, the monotone case being similar.

Let $\phi$ be a formula of size $n$. We can think of $\phi$ as a binary tree. In general, $\phi$ need not be balanced. It is not hard to show that $\phi$ always has a vertex $\psi$ corresponding to a subformula of size between $n/3$ and $2n/3$ (proof: descend from the root until you reach a subformula of size smaller than $2n/3$). Replace $\psi$ with a new formal variable $x$. The original formula is equivalent to the formula
$$
(\psi \land \phi|_{x=1}) \lor (\lnot \psi \land \phi|_{x=0}).
$$
(If $\phi$ is monotone, we don't need $\lnot \psi$.) What have we accomplished? At the cost of slightly increasing the size of the formula, we managed to get the two top levels of the formula balanced: the subformulas at depth 2 all have size between $n/3$ and $2n/3$.

We continue this process recursively with all the subformulas at depth 2. The process stops after $O(\log n)$ steps, since the subformulas at depth 2 decrease at a constant rate. Hence the final formula has depth $O(\log n)$, and so size $n^{O(1)}$. At the cost of polynomially increasing the size, we have ensured that it is balanced.