Here we can find a discussion of the Drinker paradox.
We can prove it in Hilbert-style using the axiom system of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).
In this post you can find a proof of theorem (Q3A) [see Example 8, page 130] :
$\vdash(∀x \beta \rightarrow \alpha) \leftrightarrow ∃x(\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.
From axiom 2 : $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$, with $P(x)$ as $\alpha$ and $y$ as $t$, we have :
$\vdash \forall x P(x) \rightarrow P(y)$.
Thus we have :
$\forall x P(x) \vdash P(y)$
and applying the Generalization Theorem [page 117] :
$\forall x P(x) \vdash \forall y P(y)$.
Finally, by Deduction Theorem [page 118], we conclude :
$\vdash (\forall x P(x) \rightarrow \forall y P(y))$.
Now we can apply the above theorem (Q3A), with $\forall y P(y)$ as $\alpha$ and $P(x)$ as $\beta$, where clearly, $x$ is not free in $\alpha$, to conclude :
$\vdash \exists x (P(x) \rightarrow \forall y P(y))$.