Can the converse of this predicate axiom be proved a theorem?

Question

In predicate calculus, one of the logical axioms is given like:

Let $p,q$ be any formulae in predicate calculus and variable $x$ is not free in $p$ (or doesn't occur), then the formula below is an axiom: $$ \forall x(p\to q)\to (p\to \forall x q). $$

I'm wondering if the formula below is a theorem, given $x$ does not occur in $p$: $$ (p\to \forall x q)\to \forall x(p\to q). $$

MY PROGRESS

I tried these steps of inference:

1. $p\to \forall x q$

2. $\forall x q\to q$$\qquad$(Predicate axiom)

3. $(s\to t)\wedge (t\to u)\to (s\to u)$$\qquad$(Tautology)

4. $p\to q$$\qquad$(By 1. and 2.)

5. $\forall x(p\to q)$$\qquad$(Generalization)

But I can't show these steps are correct, especially step 2. and 4.

Answer 1

The converse of the axiom is a theorem and the proof is correct.

I am accustomed to the system given in John Kelly's The Essence of Logic:

Instead of the 3rd line, Kelly employs a derived rule called transitivity of implication (TI) (proved in the chapter on propositional calculus):