$\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

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.

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}$$