Derivation of ∀x (A(x) → B(x)) → (∀x A(x) → ∀x B(x)) in Hilbert style system While it's quite easy to give a derivation of 
$$\forall x ~ \bigg(A(x) \implies B(x)\bigg) \implies \bigg(\forall x~ A(x) \implies \forall x~ B(x)\bigg)$$
in a system that contains the rule of Universal Instantiation, how do you give one in a Hilbert style system like the one in Derek Goldrei's Predicate and Propositional Calculus: A Model of Argument. His Axiom 4, 
$$\forall x (A \implies A[t/x]) \tag{Axiom 4}$$
where $t$ is free for $A$,  seems to work as a kind of UI, but I'm not that sure. What I'm trying to say is:  Does Axiom 4 warrant the inference:
$$\forall x~ (A(x) \implies B(x))$$
$$\downarrow$$
$$\text{(Apply Axiom 4)}$$
$$\downarrow$$
$$(A(x) \implies B(x))$$
...?
 A: 1)$∀x (A(x) \to B(x))$ --- premise [a]
2) $∀x A(x)$ --- premise [b]
3) $A(x) \to B(x)$ --- from 1) by Ax.4 and modus ponens
4) $A(x)$ --- from 2) by Ax.4 and modus ponens
5) $B(x)$ --- from 3) and 4) by mp
6) $∀x B(x)$ --- from 5) by Gen rule : $x$ is not free in [a] nor in [b]

7) $\vdash  ∀x (A(x) \to B(x)) \to (∀x A(x) \to ∀x B(x))$ --- from 1), 2) and 6) by Deduction theorem twice.

A: Since "Hilbert style system" is mentioned. It would be better if not using deduction theorem. I can reduce to just use it one time.
$\forall x(Ax\to Bx)$----------------------------Hyp
$\forall x(Ax\to Bx)\to(At\to Bt)$-----------Axiom 5
$\forall xAx\to At$------------------------------Axiom 5
$\forall y(\forall xAx\to By)\to(\forall xAx\to \forall yBy)$-Axiom 6
$At\to Bt$---------------------------------1,2 MP
$\forall xAx\to Bt$-----------------------------3,5 HS
$\forall y(\forall xAx\to By)$------------------------6 Gen
$\forall xAx\to \forall yBy$--------------------------4,7 HS
$\forall xAx\to \forall xBx$--------------------------Replace y by x
$\forall x(Ax\to Bx)\vdash\forall xAx\to \forall xBx$
$\vdash\forall x(Ax\to Bx)\to\forall xAx\to \forall xBx\quad$ Use deduction theorem one time.
