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.
There is no error in your sketch. My only remark is that in step 5, I would also indicate that MP is used, $[5:4+UG+MP]$ and then from 1 and 5 you get the reversed implication.