Predicate Logic, Proof of validity . How to remove negation infront of existential quantifier? $\forall x~(P(x) \to (Q(x) \lor R(x))), \lnot \exists x~(P(x) \land R(x)) \vdash \forall x~(P(x) \to Q(x))$
I am stuck on how to get rid of the negation on "$\lnot \exists x~(P(x) \land R(x))$" in this particular case. I have a relative idea of going about this sentence , where first using 2nd premise eliminating the "$\exists x$" and then getting the "$P(x_0)$" and "$R(x_0)$" respectively, then after that using "$\forall x$" elimination to get "$P(x_0) \to (Q(x_0) \lor R(x_0))$", that then allows me to use the $P(x_0)$ from previous "$P(x_0) \land R(x_0)$" to eliminate the conditional connective that allows me to have two sub-proofs to eliminate the disjunction. I can then do conditional introduction giving "$P(x_0) \to Q(x_0)$" needed and after that just introduction of $\forall x$ that gives me $\forall x~(P(x) \to Q(x))$ what I am looking for.
My problem is on how to get rid of the negation in 2nd premise in this sentence or am I going in the wrong direction on this one?
Any advice would help.
Thanks!
My attempt thus far:


 A: 
I am stuck on how to get rid of the negation on "$\lnot \exists x~(P(x) \land R(x))$" in this particular case. I have a relative idea of going about this sentence , where first using 2nd premise eliminating the "$\exists x$" and then getting the "$P(x_0)$" and "$R(x_0)$" respectively, then after that using "$\forall x$" elimination to get "$P(x_0) \to (Q(x_0) \lor R(x_0))$", that then allows me to use the $P(x_0)$ from previous "$P(x_0) \land R(x_0)$" to eliminate the conditional connective that allows me to have 2 sub proofs to eliminate the disjunction. I can then do conditional introduction giving "$P(x_0) \to Q(x_0)$" needed and after that just introduction of $\forall x$ that gives me $\forall x~(P(x) \to Q(x))$ what I am looking for.

You have the right idea. However, you should start with assuming $P(x_0)$ for an otherwise arbitrary $x_0$, then eliminate the universal quantifier in the first premise to that witness, eliminate the conditional, and thence eliminate the resulting disjunction. (Since you have $P(x_0)$ and $Q(x_0)\lor R(x_0)$ at that point.) 
In the left case, $Q(x_0)$ is trivially derived, while in the right case is where the magic happens.  From $R(x_0)$ and the assumed $P(x_0)$ derive the existance of $P(x_0)\land R(x_0)$, that is $\exists x~(P(x)\land R(x)$, which would contradict the second premise. Explode that contradiction.
Then introduce a universal quantifier, deducing $\forall x~(P(x)\to Q(x))$ as desired.
$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{~~1.~~\forall x~(P(x)\to(Q(x)\lor R(x))\hspace{10ex}\textsf{Premise}\\~~2.~~\neg\exists x~(P(x)\land R(x))\hspace{18ex}\textsf{Premise}}{\fitch{~~3.~~[x_0]\hspace{10ex}\textsf{Arbitrary Witness}}{\fitch{~~4.~~P(x_0)\hspace{10ex}\textsf{Assumption}}{~~5.~~P(x_0)\to(Q(x_0)\lor R(x_0))\hspace{10ex}\textsf{Universal Elimination}\\~~6.~~Q(x_0)\lor R(x_0)\hspace{10ex}\textsf{Conditional Elimination}\\\fitch{~~7.~~Q(x_0)\hspace{10ex}\textsf{Assumption (Left Case)}}{}\\~~8.~~Q(x_0)\to Q(x_0)\hspace{10ex}\textsf{Conditional Introduction}\\\fitch{~~9.~~R(x_0)\hspace{10ex}\textsf{Assumption (Right Case)}}{10.~~P(x_0)\land R(x_0)\hspace{10ex}\textsf{Conjunction Introduction}\\11.~~\exists x~(P(x)\land R(x))\ldots\hspace{10ex}\textsf{Existential Introduction}\\12.~~\bot\hspace{10ex}\textsf{Negation Elimination}\\13.~~Q(x_0)\hspace{10ex}\textsf{Explosion (Ex Falsum Quodlibet)}}\\14.~~R(x_0)\to Q(x_0)\hspace{10ex}\textsf{Conditional Introduction}\\15.~~Q(x_0)\hspace{10ex}\textsf{Disjunction Elimination}}\\16.~~P(x_0)\to Q(x_0)\hspace{10ex}\textsf{Conditional Introduction}}\\17.~~\forall x~(P(x)\to Q(x))\hspace{10ex}\textsf{Universal Introduction}}$
A: Basic idea: Assume P(a).  Deduce Q(a) within the scope of P(a).  
For a hint on getting rid of the negation note that existential introduction doesn't have any restrictions, does it?
More detail:
Assume (P(a)$\land$R(a)), where 'a' is a constant.  Then you can get a contradiction (hint: use existential introduction).  So, you can infer $\lnot$(P(a)$\land$R(a)).  But, then 'a' will appear and not appear anywhere else in assumptions made.  Thus, you'll have the ability to use universal introduction, to have ∀x$\lnot$(P(x)$\land$R(x)).  Then using a De Morgan law you have ∀x($\lnot$P(x)$\lor$$\lnot$R(x)).
Then assume P(a).  By universal elimination you can infer ($\lnot$P(a)$\lor$$\lnot$R(a)).  So, you can manage to get to $\lnot$R(a).  Also, derive (Q(a)$\lor$R(a)) by using the first premise and P(a).  So, you can then derive Q(a).
Then discharge P(a) yielding (P(a)$\rightarrow$Q(a)).  And note that 'a' doesn't appear in any assumptions still in effect for the last step. 
A: Instead of trying to eliminate the negation in front of the existential, use that statement as part of a proof bu contradiction.
To be a bit more specific: ypu need to show that every P is a Q. OK, so take any arbitrary object that is a P. Now assume (here the proof by contradiciotn starts) that it is not a Q. Well, by premise 1, we know the object is either a Q or an R ... but we just assumed that it was not a Q, so it must be an R. But then the object is both a P and a R, so there is something that is a p and a R (you'll probably do an existential Introduction at this point) and so that contrdicts premise 2. So, the assumption must be withdrawn, and so the object is a Q. Finally, since the object was arbitrary, we can say that any Q is an R.
Now, I don't know the specific rules of your proof system, but chances are it can implement this proof idea. Good luck!
