$\def\ha{\mathsf{HA}}\def\down{{\downarrow}}\def\mr{\mathrel{\mathbf q}}$I believe this can be proved in a fairly weak fragment of arithmetic, such as $\mathsf{I\Delta_0+EXP}$, possibly even in a polynomial-time arithmetic ($\mathsf{PV_1}$, or $\mathsf{S^1_2}$ if you prefer) if one takes care about efficient representation of programs and such things.

The hardest part is to prove

> **Theorem.** If $\ha\vdash\forall x\,\exists y\,\phi(x,y)$, there is a program $e$ such that $\ha\vdash\forall x\,(\{e\}(x)\down\land\phi(x,\{e\}(x)\down))$.

**Proof sketch:**
For any formula $\phi(\vec x)$, let $n\mr\phi(\vec x)$ denote modified realizability, defined by induction on the length of the formula:
$$\begin{align*}
n\mr\phi&\equiv\phi,\qquad\text{if $\phi$ is atomic or $\bot$,}\\
n\mr(\phi\land\psi)&\equiv((n)_0\mr\phi)\land((n)_1\mr\psi),\\
n\mr(\phi\lor\psi)&\equiv((n)_0=0\land(n)_1\mr\phi)\lor((n)_0=1\land(n)_1\mr\psi),\\
n\mr(\phi\to\psi)&\equiv(\phi\to\psi)\land\forall m\,((m\mr\phi)\to\{n\}(m)\down\land\{n\}(m)\mr\psi),\\
n\mr\exists y\,\phi(\vec x,y)&\equiv(n)_0\mr\phi(\vec x,(n)_1),\\
n\mr\forall y\,\phi(\vec x,y)&\equiv\forall y\,(\{n\}(y)\down\land\{n\}(y)\mr\phi(\vec x,y)).
\end{align*}$$
Then show by induction on the length of $\phi$ that $\ha\vdash((n\mr\phi)\to\phi)$ (easy), and show by induction on the length of a proof that if $\ha\vdash\phi(\vec x)$, then there is $e$ such that $\ha\vdash\forall\vec x\,(\{e\}(\vec x)\down\land\{e\}(\vec x)\mr\phi(\vec x))$ (tedious). Note that it is essential here that even if $\phi$ is a sentence, $e$ is not directly a numeral that realizes $\phi$, but only a program (with no input) that is supposed to output a realizer; otherwise, the whole thing would imply the existence property of $\ha$, which is not provable even in $\ha$ or $\mathsf{PA}$ itself, let alone in a much weaker theory.

> **Corollary.** If $\ha\vdash\forall x\,(\phi(x)\lor\neg\phi(x))$, there is $e$ such that $\ha\vdash\forall x\,(\{e\}(x)\down\land(\phi(x)\leftrightarrow\{e\}(x)=0))$.

Then we can follow the argument in H. Friedman, *Classically and intuitionistically provably recursive functions*:

> **Lemma.** If $\ha\vdash\phi$, then $\ha\vdash\phi^A$ for any formula $A$, where $\phi^A$ denotes [Friedman’s translation](https://en.wikipedia.org/wiki/Friedman_translation).

**Proof:** Straightforward induction on the length of the proof.

> **Theorem.** If $\ha$ proves $\forall x\,(\phi(x)\lor\neg\phi(x))$ and $\neg\neg\exists x\,\phi(x)$, then $\ha$ proves $\exists x\,\phi(x)$.

**Proof:** Let $e$ be such that $\ha\vdash\phi(x)\leftrightarrow\{e\}(x)=0$, whence $\ha\vdash\neg\neg\exists x\,\{e\}(x)=0$. Then $\ha\vdash(\neg\neg\exists x\,\{e\}(x)=0)^{\exists x\,\{e\}(x)=0}$, which is provably equivalent to $\exists x\,\{e\}(x)=0$ itself. Thus, $\ha\vdash\exists x\,\phi(x)$.