Can't go from one step to another in my proof I'm trying to proof a theorem and currently stuck at :
$$(\exists x |: Q \land \lnot R)\lor(\forall x |: \lnot P \lor R)$$
I believe I can end up with something like :
$$(\forall x|:(Q\land\lnot R)\lor(\lnot P\lor R))$$
From there I'm actually able to complete the proof, but I'm unable to explain how those two are equivalents.
I believe the answer is to use distributivity of $\lor$ over $\exists$:
$$(\exists x |: R) \Rightarrow ( P \lor (\exists x | R:Q) \equiv (\exists x | R : P \lor Q))$$
But I'm then unable to end with the expected result as I get R in the body (which is simply true in my case), but I would instead need P. Is my understanding of distributivity of $\lor$ over $\exists$ incorrect or is it just the wrong theorem to use?
Note: I'm trying to prove a theorem with the form $A\Rightarrow (B \Rightarrow C)$. I started with $B \Rightarrow C$ so I'm expecting to use a $\Leftarrow$ to come back to A.
 A: The two statements are not equivalent, nor can you even derive the second from the first.  Note that we can simply satisfy the first by making the first disjunct true, i.e. there is some object for which $Q \land \neg R$ is true.
But then we can make the second statement false simply by picking a second object for which $Q \land \neg R$ is not true, and we can also make sure that for this second object $\neg P \lor R$ is also not true by making sure that for this second object $R$ is not true, $Q$ is not true, and $P$ is true.
In sum, a simple counterexample is a two object domain where object $1$ is a $Q$ but not an $R$, and where object $2$ is a $P$, but not a $Q$, and also not a $R$
A: As far as I can see, I believe the simplest way to cast this proof, is to rewrite your original$$
(\forall x \mid \lnot R : P \Rightarrow Q) \Rightarrow ((\forall x \mid Q : R) \Rightarrow (\forall x \mid P : R))
$$ in the form $\;\ldots \land \ldots \;\Rightarrow\; \ldots\;$, and then simplify the left hand side working towards the right hand side.  You should be able to do that without introducing $\;\exists\;$.
A: 
I am basically trying to prove 
  $(∀x|¬R:P⇒Q)⇒((∀x|Q:R)⇒(∀x|P:R))\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline #2\end{array}}$

Assume every $x$ that satisfies $\neg R$ will satisfy $P\to Q$, and further assume that every $x$ that satisfies $Q$ will satisfy $R$.   Now consider the instance of any $x$ that satisfies $P$.   Such an $x$ cannot satisfy $\neg R$, because ...(insert reasons for the contradiction), so it must satisfy $R$ (in classical logic).   Discharging the assumptions deduces the required nested implication: $$\vdash (\forall x\mid\neg R:P\to Q)\to \big((\forall x\mid Q: R)\to(\forall x\mid P:R)\big)$$

$$\tiny\fitch{}{\fitch{(\forall x\mid\neg R:P\to Q)}{\fitch{(\forall x\mid Q: R)}{\fitch{[x]\mid P}{\fitch{\neg R}{\vdots\\\vdots\\R\\\bot}\\\neg\neg R\\R}\\(\forall x\mid P:R)}\\(\forall x\mid Q: R)\to(\forall x\mid P:R)}\\(\forall x\mid\neg R:P\to Q)\to \big((\forall x\mid Q: R)\to(\forall x\mid P:R)\big)}$$
