Natural Deduction Prove ∀x¬P (x) $\begin{array}{|l} \forall xP(x) \vee \forall x \neg P(x) \quad premise 
\\ \exists xQ(x) \rightarrow \neg P(x) \quad premise \\ \forall xQ(x) \quad premise
\\\hline \begin{array}{|l} \forall xP(x) \quad assumption
\\\hline \vdots \quad 
\\ \forall x\neg P(x) \quad \end{array}
\\\begin{array}{|l} \forall x\neg P(x) \quad assumption \\\hline \end{array} 
\\ \forall x \neg P(x) \quad \vee elim\\ \end{array}$
Am I on the right path to solving this or how should I be thinking about it? I think I may have strayed from the path in trying to use $\vee$ elim, just didn't see a different path to take. 
 A: Hint: you have an existential and a universal in the premises.  Assume a witness for the existance and see what happens under the assumption of $\forall x~P(x)$.
$\begin{array}{|l} \forall xP(x) \vee \forall x \neg P(x) \quad premise 
\\ \exists xQ(x) \rightarrow \neg P(x) \quad premise \\ \forall xQ(x) \quad premise
\\\hline \begin{array}{|l} \forall xP(x) \quad assumption\\\hline \begin{array}{|l}[c]~Q(c)\to\neg P(c)\quad assumption\\\hline \vdots \end{array}\\\ldots \qquad existential~elimination \\ \vdots
\\ \forall x\neg P(x) \quad \end{array}
\\\begin{array}{|l} \forall x\neg P(x) \quad assumption
\\\hline  \end{array} 
\\ \forall x \neg P(x) \quad \vee elim\\ \end{array}$
A: What you did so far is correct, and you only have to fill in the "..."s in your subproofs.
The second subproof is easy: You already got your conclusion $\forall x \neg P(x)$ as an assumption -- just reiterate (R) that line and you're done.
As for the first subproof, the idea is to derive a contradiction between $\neg P(a)$ for some individual $a$ in the second premise -- of which we know there is an instance, since we are given $\forall x Q(x)$ -- and the universal claim $\forall x P(x)$:
Assume $Q(a) \to \neg P(a)$ for an arbitrary individual $a$. By the third premise $\forall x Q(x)$ we know by universal instantiation ($\forall\!$ E) that $Q$ indeed holds of $a$. By modus ponens ($\to\!$ E), we can conclude $\neg P(a)$. But this contradicts the proposition that $P(a)$, which we get out of the assumption $\forall x P(x)$ by $\forall\!$ E, so we get a contradiction $\bot$. From this contradiction we are allowed to conclude anything thanks to ex falso quodlibet ($\bot$) -- conveniently, we can choose $\forall x \neg P(x)$ as the next conclusion. Since we were able to derive this conclusion under the assumption that $Q(a) \to \neg P(a)$ holds for some individual $a$, and by the second premise we know that at least one such individual does exist, we may apply $\exists\!$ E on the existential formula and the subproof, and thereby discharge the assumption $Q(a) \to \neg P(a)$ to conclude $\forall x \neg P(x)$ for sure.

