Natural deduction moving quantifiers I have difficulties proving with natural deduction the following:
$$Ga\rightarrow\exists xFx \vdash \exists x(Ga\rightarrow Fx)$$
Thanks for the help!
 A: The idea is to first isolate $\exists x Fx$ from the hypothesis $Ga \to \exists x Fx$ to get rid of the existential quantifier in $\exists xFx$, and then reintroduce the existential quantifier outside of $Ga \to Fx$. Formally, the derivation in natural deduction has the form below.
\begin{align}
\dfrac{
 \dfrac{
  Ga \to \exists x Fx \qquad Ga
 }{
  \exists xFx
 }\to_\text{elim} \qquad 
 \dfrac{\dfrac{[Fx]^*}{Ga \to Fx}\to_\text{intro}
}{
 \exists x (Ga \to Fx)}\exists_\text{intro}}{\exists x (Ga \to Fx)
}
\exists_\text{elim}^*
\end{align}
But there is a problem! We added an hypothesis $Ga$ which we have not discharged.
Thus, the derivation above actually proves that $Ga \to \exists x Fx, \ Ga \vdash \exists x (Ga \to Fx)$.
The next step to answer your question is then to plug the derivation above into another derivation, so that we can discharge the further hypothesis $Ga$.
The way to do that is quite technical, see below (the vertical dots stand for the derivation $Ga \to \exists x Fx, \ Ga \vdash \exists x (Ga \to Fx)$ above).
\begin{align}
\small
\dfrac{\dfrac{[\lnot\exists x (Ga \to Fx)]^\bullet \qquad \dfrac{\dfrac{\dfrac{\dfrac{[\lnot\exists x (Ga \to Fx)]^\bullet \qquad \genfrac{}{}{0pt}{0}{\genfrac{}{}{0pt}{0}{Ga \to \exists x Fx, \ [Ga]^\circ}{\vdots}}{\exists x (Ga \to Fx)}}{\bot}\lnot_\text{elim}}{Fx}\text{efq}}{Ga \to Fx}\to_\text{intro}^\circ
}{\exists x (Ga \to Fx)}\exists_\text{intro}}{\bot}\lnot_\text{elim}
}{\exists x (Ga \to Fx)}\text{raa}^\bullet
\end{align}
