Logic - Reducing a first-order logic involving a material conditional Suppose that
$$
\forall x \forall y: P(x,y) \implies Q(x)
$$
and
$$
\forall x \exists y: P(x,y)
$$
Then, can I conclude that
$$
\forall x: Q(x)
$$
If it is true, what is the rationale for it?
What I tried:
$$
\begin{align}
&\forall x \forall y: P(x,y) \implies Q(x)\\
&\iff
\forall x \forall y:\lnot P(x,y) \lor Q(x)\\
&\iff
\forall x: (Q(x) \lor \forall y:\lnot P(x,y))\\
&\iff
\forall x: (Q(x) \lor \lnot (\exists y:P(x,y)))
\end{align}
$$
Combining the result with $\forall x \exists y: P(x,y)$, I concluded that $Q(x)$ should be true for all $x$ since $\lnot (\exists y:P(x,y))$ is always false.
$$
\begin{align}
&\forall x: (Q(x) \lor \lnot (\exists y:P(x,y)))
\land \forall x \exists y: P(x,y)\\
&\iff \forall x: ((Q(x) \lor \lnot (\exists y:P(x,y))) \land \exists y: P(x,y))\\
&\iff \forall x: (Q(x) \land \exists y: P(x,y))\\
&\implies \forall x: Q(x)
\end{align}
$$
 A: 
If it is true, what is the rationale for it?

$\def\boxit#1{\bbox[lemonchiffon,0.5ex]{#1}}$We have premises of $\boxit{\forall x~\forall y:(P(x,y)\to Q(x))}$ and $\boxit{\forall x~\exists y:P(x,y)}$.   Should we take an arbitrary variable, $\boxit a$, then we infer from the second premise that there is a witness variable, call it $\boxit b$, which satisfies $\boxit{P(a,b)}$.   For these variables, we also infer from the first premise that $\boxit{P(a,b)\to Q(a)}$ will be satisfied.   Thus, by modus ponens, we infer that $\boxit{Q(a)}$ is satisfied.   Since $\boxit b$ does not occur in this statement, and $\boxit a$ is arbitrary, we have therefore shown that $\boxit{\forall x:Q(x)}$ is entailed by these premises.
$$\def\fitch#1#2{~~~~{\begin{array}{|l}#1\\\hline#2\end{array}}}\fitch{~~1.~\forall x\,\forall y:(P(x,y)\to Q(x))\hspace{3.5ex}\textsf{Premise}\\~~2.~\forall x\,\exists y:P(x,y)\hspace{14ex}\textsf{Premise}}{\fitch{~~3.~\boxed a\hspace{23.5ex}\textsf{Assumption (Arbitrary)}}{~~4.~\forall y:(P(a,y)\to Q(a))\hspace{4ex}\textsf{Universal Elimination, 1}\\~~5.~\exists y:P(a,y)\hspace{14.5ex}\textsf{Universal Elimination, 2}\\\fitch{~~6.~\boxed b~P(a,b)\hspace{13.5ex}\textsf{Assumption (Witness)}}{~~7.~P(a,b)\to Q(a)\hspace{8ex}\textsf{Universal Elimination, 4}\\~~8.~Q(a)\hspace{18.5ex}\textsf{Conditional Elimination, 6, 7}}\\~~9.~Q(a)\hspace{21.5ex}\textsf{Existential Elimination 5, 6-8}}\\10.~\forall x:Q(x)\hspace{19.75ex}\textsf{Universal Introduction, 3-9}}$$
A: That's all correct.  for that last step you can actually use the distribution of $\forall$ over $\land$ again:
$$\forall x : (Q(x) \land \exists y : P(x,y))$$
$$\Leftrightarrow$$
$$\forall x : Q(x) \land \forall x \exists y : P(x,y))$$
$$\Rightarrow$$
$$\forall x : Q(x)$$
You haven't learned formal derivations yet?
