Fix a first-order language $\mathcal{L}$ with $\bot$, and write $\neg A$ for $A\to\bot$. Let classical logic $\mathrm{CL}$ be the natural-deduction system obtained from intuitionistic first-order logic $\mathrm{IL}$ by adding the double-negation-elimination rule. Define the Goedel-Gentzen negative translation recursively by $P^N:=\neg\neg P$ for atomic $P$, $\bot^N:=\bot$, $(A\land B)^N:=A^N\land B^N$, $(A\to B)^N:=A^N\to B^N$, $(A\lor B)^N:=\neg(\neg A^N\land\neg B^N)$, $(\forall x\,A)^N:=\forall x\,A^N$, and $(\exists x\,A)^N:=\neg\forall x\,\neg A^N$. If $\Gamma\vdash_{\mathrm{CL}} A$, then $\Gamma^N\vdash_{\mathrm{IL}} A^N$, where $\Gamma^N=\{B^N:B\in\Gamma\}$.