Formal proof with first order logic axioms. How do I formally prove the following:
$$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge  Hx]$$
and by formally I mean using premises and whatever other first order logical axioms are needed.
I proved it like such, but this is not how I was supposed to do it.
$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge  Hx]$        : Distribute Quantifier
$\implies$ $[\forall y Gy \wedge \exists x Hx] \iff [\forall x\forall y Gy \wedge \exists x Hx]$ :Null Quantification
$\implies$ $[\forall y Gy \wedge \exists x Hx] \iff [\forall y Gy \wedge \exists x Hx]$
Can anyone help? Here are some of the Axioms accepted:
$$M.P: Modus Ponens$$
$$TA : Tautologies$$
$$\forall x(\delta \implies  \psi) \implies (\forall x\delta \implies  \forall x\psi)$$
$$E.I: Existential Instantiation$$
$$U.G: Universal Generalization$$
$$U.I: Universal Instantiation$$
$$E.G: Existential Generalization$$

I see you were trying Quantifier Distribution and null Quantification so I assume it is ok to  use equivalence rules.
Well, this is an immediate application of a Prenex Law:
$Q \land \exists x \phi(x) \Leftrightarrow \exists x (Q \land \phi(x))$
Where Q does not contain $x$ as a free variable.
If equivalence rules are not allowed, then we will need to know what inference rules you are allowed.
