Axioms a)-c) are a complete set of axioms for propositional logic and thus we are allowed to use in your proofs every instance of tautologies (like $\varphi \leftrightarrow \lnot \lnot \varphi$).
In addition, axioms a)-b) are enough to prove the Deduction Theorem.
Please, note that axiom 1) is wrongly stated. It must be (see your previous post ) :
$\forall x(\varphi \rightarrow \psi) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$.
In axiom 2), we have to add the proviso that $x$ is not free in $\varphi$, otherwise the formula $φ→∀xφ$ is not valid: thus, it cannot be an axiom.
Whit these corrections, axioms a)-c) plus 1)-3) form a complete set of axioms for first-order logic.
I assume that the only inference rule is modus ponens.
Having said that, the proof looks fine to me, except for the last step : what is the invoked "universal generalization" ?
Do you have also the inference rule :
$${\varphi \over \forall x \varphi}$$
If so, there are some "interference" with the deduction theorem to be checked.
Otherwise, with only modus ponens as rule, we must use the Generalization Theorem :
if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.
Added
Now the proof. We start using an instance of axiom a); the axiom is a schema. i.e. we may assert every instance of it, that is every formula obtained from the schema putting formulas whatever in place of $\varphi$ and $\psi$, provided that we substitute all occurrence of $\varphi$ (and $\psi$, and so on) with the same formula.
Thus, from :
$\vdash φ→(ψ→φ)$
putting $Bx$ in place of $\varphi$ and $Ax$ in place of $\psi$, we get 1) :
$\vdash Bx→(Ax→Bx)$.
Until 9) there are some easy steps. Then 10) is a new assumption; the "rule" is :
$\Gamma \vdash \varphi$, when $\varphi \in \Gamma$;
in our case : $\Gamma = \{ ¬(Ax→Bx) \}$.
Thus we state the temporary assumption : $\lnot (Ax \rightarrow Bx)$. We will "discharge" it in step 14) using the DT, in the same way as in step 7) we have "discharged" the temporary assumption $¬¬Bx$ introduced in step 2).
Having derived 9) :
$⊢¬(Ax→Bx)→¬Bx$
with 10) we use modus ponens to derive : $\lnot Bx$, under the above temporary assumption 10); that is 11) :
$\lnot (Ax \rightarrow Bx) \vdash \lnot Bx$.
Now we use a new instance of axiom a) : $\vdash φ→(ψ→φ)$, putting $\lnot Bx$ in place of $\varphi$ and $\lnot Ax$ in place of $\psi$. Thus, we get 12) :
$⊢¬Bx→(¬Ax→¬Bx)$.
Finally, we use modus ponens with 11) and 12) to "detach" : $(¬Ax→¬Bx)$.
But $\lnot Bx$ (we have used it in the last application of mp) "depends on" the temporary assumption 10); thus also the conclusion of mp depends on it, and we have 13) :
$¬(Ax→Bx) \vdash (¬Ax→¬Bx)$.
The last steps are easy.
Note about axiom schemata [from : Peter Smith, Types of Proof System (2010)].
Let's have an example of an axiomatic system to be going on with. In this system $\mathsf M$, to be found e.g. in Mendelson's classic Introduction to Mathematical Logic, the only
propositional connectives built into the basic language of the theory are '$\rightarrow$' and '$\lnot$' ('if ... then ...' and 'not', the same choice of basic connectives as in Frege's Begrisschrift).
The axioms are then all wffs [wee-formed formulas] which are instances of the schemata [see footnote] :
Ax1. $(A \rightarrow (B \rightarrow A))$
Ax2. $((A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow)))$
Ax3. $((\lnot B \rightarrow \lnot A) \rightarrow ((\lnot B \rightarrow A) \rightarrow B))$.
$\mathsf M$'s one and only rule of inference is modus ponens, the rule from $A$ and $(A \rightarrow C)$ infer $C$.
In this axiomatic system, a proof from the given premisses $A_1, A_2, ...A_n$ to conclusion $C$ is a linear sequence of wffs such that each wff is either :
(i) a premiss $A_i$,
(ii) a logical axiom, i.e. an instance of Ax1, Ax2 or Ax3, or
(iii) follows from two previous wffs in the sequence by modus ponens, and
(iv) the final wff in the sequence is $C$.
When there is such a proof we will write :
$A_1, A_2, ... A_n \vdash_{\mathsf M} C$.
If we can prove $C$ from the axioms alone without additional premisses, we'll say that
$C$ is a theorem, and write simply $\vdash_{\mathsf M} C$.
Footnote. 3`Instances of the schemata'? An wff is an instance of a schema (plural: schemata) if it results for systematically replacing schematic letters $A, B, C$ etc. in the schema by particular wffs - with, in a given case, the same schematic letter always being substituted by the same wff.
Going back to our example (see : step 1), from the schemata a) :
$φ→(ψ→φ)$
[which is the same as Ax1 of Peter Smith's paper] we may "generate" as many instances as we want. To do this, we need two formulas whatever to be substituded in place of shematic letters $\varphi$ and $\psi$.
Example 1) : $p$ in place of $\varphi$ and $q$ in place of $\psi$ :
$p→(q→p)$.
Example 2) : $0 = 0$ in place $\varphi$ and $1 = 0$ in place of $\psi$ :
$(0=0)→[(1=0)→(0=0)]$.
Example 3) : $Bx$ in place $\varphi$ and $Ax$ in place of $\psi$ :
$Bx→(Ax→Bx)$.
We have not "derived" $Bx$; we are using "instruction" n° (ii) of the above definition of proof :
a linear sequence of wffs such that each wff is [...] a logical axiom, i.e. an instance of Ax1, Ax2 or Ax3.
