Suppose for contradiction that $\varphi\land \lozenge\square\lnot\varphi$.
Then by our assumption, $\lozenge(\square\lnot\varphi\land \lozenge\varphi)$, equivalently $\lozenge\lnot(\square\lnot\varphi\rightarrow\square\lnot\varphi)$, equivalently $\lnot\square(\square\lnot\varphi\rightarrow\square\lnot\varphi)$.
But we have $\square\lnot\varphi\rightarrow\square\lnot\varphi$, so by necessitation $\square(\square\lnot\varphi\rightarrow\square\lnot\varphi)$, contradiction.
It's interesting that I had to use distribution to prove your axiom from B, and conversely I had to use necessitation to prove B from your axiom. Probably there would be a good explanation for this if I understood modal logic better...
For future searchability, this is Exercise 13.2(iv) on p. 254 of Hughes and Cresswell A New Introduction to Modal Logic. We are to prove $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ in the first-order modal logic S4.2 with Barcan's formula.
By the law of excluded middle, either $\exists y\lozenge\square F(y)$ or $\lnot \exists y\lozenge\square F(y)$.
Case 1: $\exists y\lozenge\square F(y)$.
By S4, $\square F(y)\rightarrow \square\square F(y)$ is a theorem. By necessitation and K (and taking contrapositives twice), $\lozenge\square F(y)\rightarrow \lozenge \square\square F(y)$ is a theorem. As an instance of S4.2, $\lozenge \square\square F(y)\rightarrow \square \lozenge \square F(y)$, so $\lozenge\square F(y)\rightarrow \square \lozenge \square F(y)$ is a theorem.
Now by first-order logic, $\lozenge\square F(y)\rightarrow \forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem, so by necessitation and K, $\square\lozenge\square F(y)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem. Combining with the result of the previous paragraph, $\lozenge\square F(y)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem.
By our Case 1 assumption and first-order logic, we obtain $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$, as desired.
Case 2: $\lnot \exists y\lozenge\square F(y)$. This is equivalent to $\forall x\square\lnot \square F(x)$.
By first-order logic, $\forall x\lnot\square F(x)\rightarrow \forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem, so by necessitation and K, $\square\forall x\lnot\square F(x)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem. As an instance of Barcan's formula, $\forall x\square\lnot \square F(x)\rightarrow \square\forall x\lnot\square F(x)$. So $\forall x\square\lnot \square F(x)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem.
By our Case 2 assumption, we get $\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$. Adding the existential quantifier, $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$, as desired.
[Note that this last step assumes that our underlying first-order logic has existential import (i.e. is sound and complete for non-empty structures). I haven't checked that the system described in Hughes and Cresswell has existential import, but I assume it does - otherwise no sentence beginning with an existential quantifier is provable, since such a sentence is false on empty domains.]
Let me add something about the semantic motivation for this proof. I believe the the system in question (S4.2+Barcan's formula) is sound and complete for first-order non-empty constant domain Kripke frames which are directed preorders.
The desired sentence $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ says that there is some $y$ in world $w_1$ such that for every world $w_2\geq w_1$ and every $x$ in $w_2$, either (1) there is some world $w_3\geq w_2$ such that $F(x)$ is false at $w_3$, or (2) there is some world $w_3'\geq w_2$ such that $F(y)$ is true "on the cone above $w_3'$" (at every world $w_4\geq w_3'$).
Well, the easiest way to make (2) hold is if there is some $y$ in $w_1$ such that $F(y)$ is true on some cone above $w_1$. Indeed, if there is some world $v\geq w_1$ so that $F(y)$ is true on the cone above $v$, then for every world $w_2\geq w_1$ (and any $x$, but the choice of $x$ is irrelevant), since the frame is directed, we can pick some $w_3'$ such that $w_3'\geq v$ and $w_3'\geq w_2$. And since $F(y)$ is true on the cone above $v$, it is true on the cone above $w_3'$, so (2) holds. This semantic argument is formalized by the proof of Case 1 above.
On the other hand, suppose that there is no $y$ in $w_1$ such that $F(y)$ is true on some cone above $w_1$. Note that for every $w_2\geq w_1$ and every $x$ in $w_2$, it is not the case that $F(x)$ is true on the cone above $w_2$. Indeed, since our domains our constant, $x$ is also in $w_1$, and picking $y = x$ would contradict our assumption. This exactly means that there is some $w_3\geq w_2$ such that $F(x)$ is false at $w_3$. So picking any $y$ in $w_1$ (the choice is irrelevant), we have seen that (1) holds. This semantic argument is formalized by the proof of Case 2 above.
Best Answer
Since $\lnot(q\land\lozenge p)$ is provable, then it is a theorem and the necessitation rule can be applied.
Do so.