$\let\ET\bigwedge\let\LOR\bigvee\let\EQ\Leftrightarrow$The property is true for extensions of K (i.e., normal modal logics). You didn’t really describe the proof system you are interested in, but based on the discussion in the question, I will assume it is a Hilbert-style proof system with the rules of modus ponens and necessitation, and substitution instances of a fixed set of axioms, including a complete axiomatization of classical propositional logic, and the distributivity axiom of K. (It seems that you also allow substitution to be used as a rule. I prefer the formulation I gave with no substitution rule, but axioms schemata closed under substitution, because it has nicer structural properties. Of course, one can simulate schemata in the other system by an explicit application of substitution on the base form of the axiom.)
First, note that the “stronger property” putting a bound on the number of variables is trivially equivalent to the original formulation: given a proof of a formula $A$, you can uniformly substitute a fixed formula (e.g., $\bot$ if it’s in the language, or a variable from $A$) in all formulas in the proof for each variable which does not occur in $A$, obtaining a proof of $A$ which only involves variables from $A$.
Let me define a Boolean substitution to be a substitution $\sigma$ such that $\sigma(p)$ is a Boolean formula (i.e., $\Box$-free) for every variable $p$.
Theorem: Let $S\cup\{A\}$ be a set of formulas of modal degree $\le1$. If $\vdash_{\mathrm K\oplus S}A$, then $A$ has a derivation using
(degree-$1$ instances of) classical propositional tautologies, and the rule of modus ponens,
axioms $\Box B$, where $B$ is a $\Box$-free classical tautology, and Boolean substitution instances of $\Box(p\to q)\to(\Box p\to\Box q)$,
Boolean substitution instances of $B\in S$.
Moreover, all formulas in the proof use only variables occurring in $A$.
Proof:
Assume that the conclusion fails. Unless stated otherwise, all formulas below are required to use only the variables from $A$. By the completeness of classical propositional logic, there exists a Boolean assignment $v$ to variables and boxed Boolean formulas such that $v(A)=0$, but $v(B)=1$ for every axiom of type (2), (3). We will construct a Kripke model based on an $S$-frame where $A$ is false.
Let $\{p_0,\dots,p_{n-1}\}$ be an enumeration of all variables occurring in $A$, and if $e$ is any Boolean assignment $e\colon\{p_i:i<n\}\to\{0,1\}$, put
$$p^e:=\ET_{e(p_i)=1}p_i\land\ET_{r(p_i)=0}\neg p_i.$$
We can write an arbitrary Boolean formula $B$ in the full conjunctive normal form
$$\vdash_{\mathrm{CPC}}B\leftrightarrow\ET_{e(B)=0}\neg p^e.$$
Since $v$ makes true all axioms of type (2), we have
$$\tag{$*$}v(\Box B)=v\Bigl(\ET_{e(B)=0}\Box\neg p^e\Bigr).$$
Let $e_0$ be the restriction of $v$ to variables, and put
$$E=\{e:v(\Box\neg p^e)=0\}.$$
Define a Kripke model $M=\langle W,R,\models\rangle$ by
\begin{align*}
W&=E\cup\{e_0\},\\
e\mathrel R e'&\EQ\begin{cases}
e'\in E&\text{if $e=e_0$,}\\
e=e'&\text{otherwise,}
\end{cases}\\
e\models p_i&\EQ e(p_i)=1.
\end{align*}
In other words, $M$ is a tree of height $\le2$ with root $e_0$, and reflexive leaves $e\in E\smallsetminus\{e_0\}$. The root is reflexive iff $e_0\in E$. It follows immediately from $(*)$ and the definition that
$$\tag{$*{*}$}v(B)=1\iff M,e_0\models B$$
for every formula $B$ of degree $\le1$, in particular $M,e_0\nvDash A$.
It remains to verify that $\langle W,R\rangle$ is an $S$-frame. Since every subset $X\subseteq W$ is definable by a Boolean formula in $M$ (namely, $\LOR_{e\in X}p^e$), it suffices to show that $M$ satisfies all Boolean substitution instances of $S$-axioms. Every such instance $B$ is an axiom of the type (3), hence $(**)$ gives immediately that $M,e_0\models B$. In order to verify $M,e\models B$ for $e\ne e_0$, let $\theta$ be the Boolean substitution
$$\theta(p_i)=\begin{cases}\top&\text{if $e(p_i)=1$,}\\\bot&\text{otherwise.}\end{cases}$$
Then
$$\tag{$*{*}{*}$}M,e'\models\theta(C)\iff M,e\models C$$
for every $e'\in W$ and every formula $C$ by induction on the complexity of $C$. (The induction step for $\Box$ needs that $e_0$ has a successor, i.e., $E$ is nonempty. This follows from the assumption $e\ne e_0$.) Since we already know that $M,e_0\models\theta(B)$, we obtain $M,e\models B$ by taking $C=B$ and $e'=e_0$ in $(*{*}*)$.
