Why universal instantiation cannot be used here? I have a following sentence: 

$$\forall x~(Fx \to \forall y~(Fy \to Gy)) ~\vdash~ \forall x~(Fx \to Gx) $$

Why I cannot use UI twice and get: 

$$Fa \rightarrow (Fa \rightarrow Ga) $$

This is my proof:
1) $\forall x~(Fx \to \forall y~(Fy \to Gy))$
$\quad$2) $Fa \to (Fa \to Ga)$
$\qquad$3) $Fa$ (Assumption)
$\qquad$4) $Ga$ (From 2,3)
$\quad$5) $Fa \to Ga$
6) $\forall x~(Fx \to Gx) $
And the second line was marked as the wrong one by somehow.
Thanks in advance.
 A: You can use Universal Instantiation(Elimination) twice.   You just cannot do it immediately.   You must instantiate the universal $x$, raise the assumption of $Fa$, modus ponens, and then instantiate the universal $y$ (to the same arbitrary $a$).   After that your proof continues as you wanted.
$$\def\fitch#1#2{\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{1.\quad \forall x~(Fx\to \forall y~(Fy\to Gy))\quad\text{Premise} }{\fitch{[a]}{2.\quad Fa \to(\forall y~(Fy\to Gy))\quad~~1,\forall\text{Elim}\\\fitch{3.\quad Fa\qquad\qquad\qquad\qquad\quad~~\text{Assume}}{4.\quad \forall y~(Fy\to Gy)\qquad\qquad~~~2,3,\to\text{Elim (modus ponens)}\\ 5.\quad Fa\to Ga\qquad\qquad\qquad~~~ 4,\forall\text{Elim}\\6.\quad Ga\qquad\qquad\qquad\qquad\quad~~ 3,5,\to\text{Elim}}\\7.\quad Fa\to Ga\qquad\qquad\qquad\quad~3,6\to\text{Intro}}\\8.\quad \forall x~(Fx\to Gx)\qquad\qquad\quad~~ 7,\forall\text{Intro}}$$
A: UI allows us to deduce $\phi$ from  $(\forall x)(\phi)$ and nothing more.
In your case, it seems like you have tried to deduce $Fa\to \phi$ from $Fa\to (\forall y)(\phi)$ with a single application of UI. This is an invalid use of UI.
A: Universal instantiation says 
$$
\forall_x\phi(x)\Rightarrow\phi(a)
$$
So, in your case you can get
$$
Fa\Rightarrow\forall_y(Fy\Rightarrow Gy)
$$
But, you have by UI that $\forall_y(Fy\Rightarrow Gy)\Rightarrow(Fa\Rightarrow Ga)$ so, by transitivity, $Fa\Rightarrow(Fa\Rightarrow Ga)$
