Distribution of universal quantifier with free variables. My question is regarding the validity of the following statement:
$$ (\forall a (\phi \implies \psi)) \equiv (\phi \implies \forall a \psi ),$$
provided, of course, there are no free occurrences of $a$ in $\phi$.
I am using the axiom system from Hughes and Cresswell, namely,
(US) $\forall a \phi \implies \phi [a / b]$ (N.B. $\phi[a/b]$ denotes a bound alphabet variant of $\phi$ with no bound $b$, then replacing every free $a$ with free $b$).
(UG) From $\phi \implies \psi$ infer $\phi \implies \forall a \psi$, provided $a$ is not free in $\phi$.
(MP) Modus Ponens. 
I also have some modal axioms in play but I assume they are irrelevant. In the book they list as a theorem:
$$ (\forall a (\phi \implies \psi)) \implies (\phi \implies \forall a \psi ),$$
provided there are no free occurrences of $a$ in $\phi$. (Which is clearly a straightforward application of (1)+MP and then (2).) I believe the other direction should follow from a rather similar argument, but seeing as the book did not list such a equivalence as a theorem, but merely a one sided implication, I am second guessing myself. Anyway, a sketch:
$$(\phi \implies \forall a \psi ) \quad [1: Assumption]$$
$$(\forall a \psi \implies \psi[a/a] )\quad  [2: US]$$
$$(\phi \implies \psi[a/a])  \quad [3: 1+2+MP]$$
$$(\phi \implies \forall a \psi ) \implies (\phi \implies \psi[a/a])  \quad [4: 1+3]$$
$$\forall a(\phi \implies \psi[a/a]) \quad [5: 4+UG]$$
Then since bound alphabetic variants are material equivalents, this delivers the result. Now, I'm a bit new to the whole logic thing so any errors or omissions would be very helpful.

My sequences of transformation is as follow:
$$
  \forall a (\phi \Rightarrow \psi)
$$
$$
  \equiv~
  \forall a (\neg\phi \vee \psi)
$$
$$
  \equiv~
  \neg\phi \vee \forall a (\psi)
$$
$$
  \equiv~
  \phi \Rightarrow \forall a (\psi)
$$
Note that from step 2 to 3, since $a$ does not occur free in $\phi$, hence $\forall a (\neg\phi \vee \psi) ~~ \equiv ~~ \neg\phi \vee \forall a (\psi)$.
