$\vdash \neg\alpha\rightarrow(\alpha\rightarrow\beta)$ without deduction theorem I wish for a formal proof for $\vdash\neg\alpha\rightarrow(\alpha\rightarrow\beta)$ which doesn't use deduction theorem. 
I use the standard axiomatic system:
$\alpha\rightarrow(\beta\rightarrow\alpha)$
$\alpha\rightarrow(\beta\rightarrow\gamma)\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma))$
$(\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow \beta)$
Using axiom 2 we get:
$$(\neg\alpha \rightarrow((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)))\rightarrow((\neg\alpha \rightarrow(\neg\beta\rightarrow\neg\alpha))\rightarrow(\neg\alpha\rightarrow(\alpha\rightarrow\beta)))$$
which is very promising casue the second expresion is axiom 1, and the expression:$(\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)$ can be proved using deduction theorem in the next manner:
$1. \neg\beta\rightarrow \neg \alpha$ assumption 
$2.\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta))$  $A2$ 
$3. (\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow\beta)$  $A3$
$4. (\neg\beta\rightarrow\alpha)\rightarrow\beta) $ by MP $1$ from $3$
$5. (\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow(\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta))$ $A1$
$6. (\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta))$ MP by 4
$7. ((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta))$  MP 6 from 2
$8.(\alpha\rightarrow(\neg \beta\rightarrow \alpha) $ A1
$9. \alpha\rightarrow \beta$ MP 7 using 8
I was trying to reverse the proof by seduction theorem using the method by which the Deduction Theorem is proved. So, I need to prove $\neg\beta \rightarrow \neg\alpha \rightarrow (step(i))$ when $step(i)$ is each of the step in the proof demonstrated above. Doing so (as you may see below) lead me to the next conclusion:
if one proves :
$((\neg\beta \rightarrow\neg\alpha)\rightarrow((\alpha\rightarrow(\neg\beta\rightarrow\alpha))\rightarrow(\alpha \rightarrow\beta))) \rightarrow(((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow(\neg\beta\rightarrow\alpha)))\rightarrow((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta)))$
The second expression can be proved by using 2 times Axiom 1.
For the first expression which I'm stuck in, I tried to prove:
$(\alpha\rightarrow(\neg\beta\rightarrow\alpha))\rightarrow(\alpha \rightarrow\beta))$ And then using Axiom 1 , but I realized that's can't be proved without assumption cause it is not a tautology! the first expression is Axiom 1 so it is tautology, then in case $\alpha\rightarrow\beta$ is not True ($\alpha = T, \beta = F)$ we get a False statement.
Maybe I took the wrong path? is it another way to solve it?
Also, it is worth to mention that this question comes from previous attempt for an other proof I am still trying to make (and I think, this proof is the key for the other):Formally proving $p\wedge q \rightarrow p$

Reversing the Deduction theorem usage:
$1^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow(\neg\beta\rightarrow \neg \alpha)$ . The same pattern as to prove $\alpha \rightarrow \alpha$
$2^*.\vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow (\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta)))$  Prooving a formula of the pattern $\gamma\rightarrow Axiom$ can be done by using Axiom1. 
$3^*.\vdash (\neg\beta\rightarrow \neg \alpha)\rightarrow ((\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow\beta))$  same pattern as $2^*$
$4^*. \vdash (\neg\beta\rightarrow \neg \alpha)\rightarrow ((\neg\beta\rightarrow\alpha)\rightarrow\beta)) $ This is an Axiom3 pattern.
$5^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow ((\neg\beta \rightarrow\alpha)\rightarrow\beta)\rightarrow(\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)))$ same pattern as $2^*$ $\gamma \rightarrow Axiom$
$6^*.\vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow ( (\alpha\rightarrow((\neg\beta \rightarrow\alpha)\rightarrow\beta)))$ MP by 4
This is the formula which I don't succeed to prove. 
$7^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow (((\alpha\rightarrow(\neg \beta\rightarrow \alpha))\rightarrow(\alpha\rightarrow \beta)))$  MP 6 from 2
$8^*. \vdash(\neg\beta\rightarrow \neg \alpha)\rightarrow((\alpha\rightarrow(\neg \beta\rightarrow \alpha)) $ A1
$9^*. \vdash (\neg\beta\rightarrow \neg \alpha)\rightarrow (\alpha\rightarrow \beta)$ MP 7 using 8
 A: Hint
As said, the proof is simple and (very) boring.
We have to start from the derivation using DT (see e.g. Mendelson ) an "expurgate" the calls to DT: we have to do it one-by-one.
Thus, starting from the derivation $\lnot B, B \vdash C$ we have firstly to produce the new derivation $\lnot B \vdash B \to C$.
I'll follow Mendelson's original derivation :
1') $\lnot B$ --- Hyp
3') $\vdash B \to (\lnot C \to B)$ --- Ax.1
4') $\vdash B \to (\lnot B \to (\lnot C \to \lnot B))$ --- derived from the suitable Ax.1  : $\vdash (\lnot B \to (\lnot C \to \lnot B)) \to [B \to (\lnot B \to (\lnot C \to \lnot B))]$ with Ax.1 and mp
5') $B \to \lnot B$ --- derived from Ax.1 : $\lnot B \to (B \to \lnot B)$ with 1') and mp
6') $B \to (\lnot C \to \lnot B)$ --- derived from Ax.2 with 4') and 5') by mp twice
7') $\vdash [B \to ((\lnot C \to \lnot B) \to ((\lnot C \to B) \to C))] \to [(B \to (\lnot C \to \lnot B)) \to (B \to ((\lnot C \to B) \to C))] \text {  --- Ax.2}$
8') $\vdash B \to ((\lnot C \to \lnot B) \to ((\lnot C \to B) \to C))$ --- derived from Ax.3 with suitable Ax.1 and mp
9') $\vdash (B \to (\lnot C \to \lnot B)) \to (B \to ((\lnot C \to B) \to C))$ --- derived 7') and 8') by mp
10') $B \to ((\lnot C \to B) \to C)$ --- derived from 9') and 6') by mp

11') $B \to C$ --- derived from Ax.2 with 3') and 10') by mp twice.

A: My answer is:
$$\begin{array}{r|ll}
1 & \neg\alpha\rightarrow(\neg\beta\rightarrow\neg\alpha) & Ax. 1\\
2 & (\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta) & Ax. 3\\
3 & (\neg\alpha\rightarrow(\neg\beta\rightarrow\neg\alpha))\rightarrow(((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta))\rightarrow(\neg\alpha\rightarrow(\alpha\rightarrow\beta))) & Ax. 2\\
4 & ((\neg\beta\rightarrow\neg\alpha)\rightarrow(\alpha\rightarrow\beta))\rightarrow(\neg\alpha\rightarrow(\alpha\rightarrow\beta)) & 1,3,MP\\
5 & \neg\alpha\rightarrow(\alpha\rightarrow\beta) & 2,4,MP
\end{array}$$
