I am tasked to find a proof of $\vdash \exists x (\phi \implies \forall x \phi)$ by using the Hilbert axioms. I've been trying for about 2 hours. I tried using the results from the previous parts of the exercise below. I am also allowed to use substitution instances of tautologies (i.e $\vdash p \implies p$ implies $\vdash \phi \implies \phi$ where $p$ is a propsitional variable and $\phi$ is a first-order formula), that $\exists x$ is defined as $\neg \forall x \neg$, and the standard meta-theorems like proof by contradiction.
Basically I've tried to work backwards:
$$\vdash \exists x (\phi \implies \forall x \phi)$$ $$\vdash \forall x (\phi \implies \forall x \phi)$$ $$\vdash (\phi \implies \forall x \phi)$$
This last step seems impossible to prove, as it would have me show that if a property is true for some x then it is true for all $x$ (obviously not true if $\phi$ is taken to be "is even")
Similarly I tried invoking part (c)
$$\vdash \exists x (\phi \implies \forall x \phi)$$
$$\vdash \forall x (\phi \implies \forall x \phi)$$
$$\vdash (\exists x \phi \implies \forall x \phi) \implies \forall x(\phi \implies \forall x \phi)$$
Again, this would require to show that if a propery is true for some x then it is true for all $x$.
The only other way to introduce an $\exists$ as the "main connective" is by (a). But that seems to go nowhere as well.
Hilbert system is well known to be very cumbersome to prove some straightforward result compared with natural deduction systems, especially for this non-trivial Drinker Paradox sentence and you don't even have the useful deduction meta-theorem. Since we know it'll be a little hard (as the last exercise in your book) so we may stand upon a known result from prenex normal form in predicate calculus that $\vdash (∀x\phi → \psi) \to ∃x(\phi → \psi)$, where $x$ does not occur free in $\psi$. So with this known theorem we can prove your result based solely on your system in only 7 steps as follows:
$\vdash (\forall x \phi → \forall x \phi) \to ∃x(\phi → \forall x \phi)~~~~~$ ...known theorem
$\vdash (\forall x \phi→((\psi→\forall x \phi) → \forall x \phi))→((\forall x \phi→(\psi→\forall x \phi))→(\forall x \phi→ \forall x \phi))~~~~~$ ...Ax 2
$\vdash \forall x \phi→((\psi→\forall x \phi)→\forall x \phi)~~~~~$ ...Ax 1
$\vdash (\forall x \phi→(\psi→\forall x \phi))→(\forall x \phi→\forall x \phi)~~~~~$ ...MP from 2, 3
$\vdash \forall x \phi→(\psi→\forall x \phi)~~~~~$ ...Ax 1
$\vdash \forall x \phi→\forall x \phi~~~~~$ ...MP from 4, 5
$\vdash \exists x (\phi \to \forall x \phi)~~~~~$ ...MP from 1, 6. Done!
Now sketch a proof of this known theorem in your specific formal system. As discussed in comments we only have one way to prove any result including $\exists$ quantifier in your system, so after plugin $\lnot \forall \lnot$ we 'd better use proof by negation technique to initally assume $\forall x \lnot (ϕ→ψ)$ where $x$ does not occur free in $ψ$, given the assumption $(∀xϕ→ψ)$. Now perhaps it's clear how to formally proceed with the given assumption and use your Axiom 4 (universal instantiation) to derive at $\bot$, thus our known theorem is proved...