Is my proof of $\vdash (\forall x)(B \implies C) \implies ((\forall x)B \implies (\forall x)C)$, without using deduction theorem, correct?

Question

I'm reading "Introduction to Mathematical Logic" from Mendelson and I'm currently reading chapter two "first-order logic and model theory". I tried to derivate ⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C) without using deduction theorem. Axioms are:

(A1): B ⇒ (C ⇒ B)

(A2): (B ⇒ (C ⇒ D)) ⇒ ((B ⇒ C) ⇒ (B ⇒ D))

(A3): (¬C ⇒ ¬B) ⇒ ((¬C ⇒ B) ⇒ C)

(A4): (∀xi)B(xi) ⇒ B(t)

(A5): (∀xi)(B ⇒ C) ⇒ (B ⇒ (∀xi)C)

Rules are :

1. Modus ponens: C follows from B and B ⇒ C. (MP)

2. Generalization: (∀xi)B follows from B. (Gen)

In orther to make my derivation simple (since my question is about first orther axiomatic and not propositional axiomatic) I'm going to assume as proven this theorem (T1): (B ⇒ (C ⇒ D)) ⇒ (C ⇒ (B ⇒ D)).

Also I'm going to use two corollarys:

1. corollary 1: B ⇒ C, C ⇒ D ⊢ B ⇒ D which cames from (A2)
2. corollary 2: B ⇒ (C ⇒ D) ⊢ C ⇒ (B ⇒ D) which cames from (T1)

My derivation:

⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C):

1. (∀x)(B ⇒ C) ⇒ (B ⇒ (∀x)C) (A5) axiom 5
2. B ⇒ ((∀x)(B ⇒ C) ⇒ (∀x)C)) corollary 2 applied in 1
3. (∀x)B ⇒ B (A4)
4. (∀x)B ⇒ ((∀x)(B ⇒ C) ⇒ (∀x)C)) corollary 1 applied in 2,3
5. (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C) corollary 2 applied in 4

Is my derivation correct?