Existential and universal quantifiers and implication

Question

$[p\rightarrow \forall x.P(x)]\equiv \forall x.[p\rightarrow P(x)]$ (1)
$[(\forall x.P(x))\rightarrow p]\equiv \exists x[P(x)\rightarrow p]$ (2)

to prove $\exists x \forall y.P(x,y)\rightarrow \forall y\exists x.P(x,y)$ (3)

apply (1) and (2) to $\forall x\forall y[\forall y.P(x,y)\rightarrow \exists x.P(x,y)]$ (4) to prove (3)

where (4) in turn can be deduced from $\forall x.P(x,y)\rightarrow P(x,y)$ and $P(x,y)\rightarrow \exists x.P(x,y)$

I cannot understand how to get (3) out of (1) and (2)

Thanks in advance.

Answer 1

apply (1) and (2) to $∀x∀y[∀y.P(x,y)→∃x.P(x,y)]$ (4) to prove (3).

Applying (1), due to the fact that $y$ is not free in $∀y.P(x,y)$, from (4) we get $∀x[∀y.P(x,y)→∀y∃x.P(x,y)]$.

Applying the Prenex Normal Form equivalence: $(\exists x\phi )\rightarrow \psi \equiv \forall x(\phi \rightarrow \psi )$ to the last formula, due to the fact that $x$ is not free in $∀y∃x.P(x,y)$ we get:

(3) $\ \ ∃x∀y.P(x,y)→∀y∃x.P(x,y)$.

Answer 2

It seems I understood:
$\forall x\forall y[\forall y.P(x,y)\rightarrow \exists x.P(x,y)] = \forall x[\forall y.P(x,y)\rightarrow \forall y \exists x.P(x,y)] = \forall x[\neg\forall y.P(x,y)\vee \forall y \exists x.P(x,y)] = \forall x \neg \forall y.P(x,y)\vee \forall y \exists x.P(x,y) = \neg \exists x \forall y.P(x,y)\vee \forall y \exists x.P(x,y) = \exists x \forall y.P(x,y)\rightarrow \forall y \exists x.P(x,y)$