Deducing $(\lnot B) \to A$ from $\lnot A \to B$ using Hilbert deductive system As the title says, I've been trying to prove this:
$(\lnot A \to B) \vdash (\lnot B) \to A)$
but unfortunately keep winding up with crazy long steps and then I have no idea where to go. The only axioms I can use are:
\begin{gather}
A \to (B \to A), \tag{Ax1} \\[0.1in]
\big(A \to (B \to C)\big) \to \big((A \to B) \to (A \to C)\big), \tag{Ax2} \\[0.1in]
(\neg B \to \neg A) \to (A \to B), \tag{Ax3} \\[0.1in]
A \to \neg (\neg A). \tag{Ax4}
\end{gather}
Any help would be greatly appreciated. I thought about doing $(\mathrm{Ax2})$ first to get the $B$ and $A$ rearranged, followed by $(\mathrm{Ax3})$, but then I got lost there. 

First, Ax4 is provable from the first three axioms.
Second, I'll suggest that you prove this handy formula: {(A→B)→[(C→A)→(C→B)]}.  You can prove it from axioms 1 and 2 only, and you only need to use modus ponens/detachment three times to prove it.
Now you can hopefully solve this yourself.  If note, the following information may prove useful.  But, to encourage you to do a little thinking, I've made it a bit harder to read.
 Now since you have detachment, that formula tells you that if you have, in Polish/Lukasiewicz notation, Cab and Cca, you can infer Ccb.  Thus, if you have CaNNb and CNaa, you can infer CNaNNb.  Then make CNaNNb into the antecedent of axiom 3 and you can detach CNba. 
