With the axioms you gave, the formula is not provable. I've used Mace to find a counter-model, which consists in interpreting "$\neg$" as an operator that always outputs $F$, irrespective of the input truth value. The arrow "$\rightarrow$" is to be interpreted standardly (since A1 and A2 indeed are axioms that capture the material conditional). Along these lines, you can now build a truth table; it will validate all the axioms but disvalidate $(\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)$.
For your information, I've used Mace on the following input. As assumptions, I chose
Thm(x) & Thm(f(x,y)) -> Thm(y).
Thm(f(x,f(y,x))).
Thm(f(f(x,f(y,z)),f(f(x,y),f(x,z)))).
Thm(f(f(f(g(x),x),x),f(f(x,y),f(g(y),g(x))))).
As the goal, I chose
Thm(f(f(g(x),g(y)),f(y,x))).
Naturally, "Thm" is the predicate for theoremhood. "f" is the functor for "$\rightarrow$", and "g" is the functor for "$\neg$". The first line says theoremhood is closed under Modus Ponens. The next three lines are translations of the axioms. The goal line is a translation of your formula.
Reply to Levitan's comment: You can choose different output formats which may vary in readability. I find the format "cooked" quite readable; it gives you:
% number = 1
% seconds = 0
% Interpretation of size 2
c1 = 0.
c2 = 1.
g(0) = 0.
g(1) = 0.
f(0,0) = 1.
f(0,1) = 1.
f(1,0) = 0.
f(1,1) = 1.
- Thm(0).
Thm(1).
There you see:
- The model has two object in its domain, $0$ and $1$, which we can naturally interpret as false and true, respectively.
- An interpretation for $g$, which I put in place of $\neg$. In an interpretation of $0$ and $1$ as truth values, it accepts truth values as input, and outputs a truth value. In this case, it always outputs $false$.
- Similarly for the two placed functor $f$.
- Finally, theoremhood is interpreted such that the Truth (every true sentence, or more precisely every term that denotes $1$) is a theorem, and falsity isn't a theorem - quite what we'd expect.
This will yield the following truth table:
$$\begin{array}{cc|c}
A & B & \neg A & \neg B & (\neg A \rightarrow \neg B) & (B \rightarrow A) & (\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A) \\
\hline
T & T & F & F & T & T & T \\
T & F & F & F & T & T & T \\
F & T & F & F & T & F & F \\
F & F & F & F & T & T & T \\
\end{array}$$