Proving predicate logic argument validity? I spent the past hour pondering on possible solutions for the following task, which is basically to prove the argument validity. 
$$\forall x\forall y(P(x, y) \rightarrow Q(x))   \vdash \forall x \exists yP(x, y) \rightarrow \forall xQ(x)$$
Any ideas?
Thanks a bunch!
 A: In natural deduction system, take the premiss and temporarily assume $\forall x\exists yP(x, y)$.
Instantiate the premiss and the temporary assumption with the parameter $a$, to get

$\forall y(P(a, y) \to Q(a))$
$\exists yP(a, y)$

With a view to using existential elimination, instantiate the existential with a new parameter. WE get

$\quad|\quad P(a, b)$
$\quad|\quad P(a, b) \to Q(a)$.

modus ponens gives us

$\quad|\quad Q(a)$.

Since this doesn't involve $b$ we can discharge the assumption at the beginning of the sub proof to get

$Q(a)$

We can universally quantify as $a$ occurs in no assumption this depends on to get

$\forall xQ(x)$

Discharge the initial temporary assumption by conditional proof and we are done.
A: As explained in the comments, you can prove this by means of the method of analytic tableaux. You assume $$\neg ((\forall x\forall y(Pxy\rightarrow Qx))\to ( \forall x \exists yPxy \rightarrow \forall xQx))$$ then apply a series of contradiction-hunting rules to get
,
which is closed; that is, each of its paths end in contradictions. Hence $$(\forall x\forall y(Pxy\rightarrow Qx))\to ( \forall x \exists yPxy \rightarrow \forall xQx),$$ which is equivalent to $$\forall x\forall y(Pxy\rightarrow Qx)\vdash  \forall x \exists yPxy \rightarrow \forall xQx.$$ The explanation for this last step is beyond my ability just yet.
This can then be used to construct a proof like Peter's as Mauro describes in the comments.
