$\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!


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}}$