Prove $ (∀x_1 (∃x_2 (p(x_1, x_2) ⇒ (∀x_2 p(x_1, x_2)))))$ Can u help show that this is a theorem? $ (∀x_1 (∃x_2 (p(x_1, x_2) ⇒ (∀x_2 p(x_1, x_2)))));$ 
I was trying to use the deduction theorem but i hit a wall. Can u help me out using derivatives and Hilbert Calculus? 
 A: "English" answer:
Fix any $x_1,\,x_2$. If $p(x_1,\,x_2)$ is false, the required implication is vacuously true. If $x_2$ cannot be chosen so that $p(x_1,\,x_2)$ is false, our choice of $x_1$ has obtained $\forall x_2 (p(x_1,\,x_2))$, so again the implication succeeds.
HC answer:
$$\exists x_2(\neg p(x_1,\,x_2))\implies(p(x_1,\,x_2)\implies \forall x_3 (p(x_1,\,x_3)))$$
$$\not\exists x_2(\neg p(x_1,\,x_2))\implies\forall x_3(p(x_1,\,x_3)),\,\implies(p(x_1,\,x_2)\implies\forall x_3(p(x_1,\,x_3)))$$
Then use $(q\implies r)\land (\neg q\implies r)\implies r$.
A: Hint
In this post you can find an Hilbert-style proof of :

$⊢(∀xβ → α) ↔ ∃x(β → α)$, provided that $x$ is not free in $\alpha$.

We have to consider :

$∀x_2p(x_1,x_2) \to ∀x_2p(x_1,x_2)$;

it is an instance of the propositional tautology : $\vdash A \to A$, and thus is a theorem.
Now we apply the equivalence above to it, due to the fact that $x_2$ is not free in $∀x_2p(x_1,x_2)$ to get :


$\vdash ∃x_2 \ (p(x_1,x_2) \to ∀x_2p(x_1,x_2))$.


The last step is obtained with Generalization:


$\vdash ∀x_1 \ ∃x_2 \ (p(x_1,x_2) \to ∀x_2p(x_1,x_2))$.


