I'm able to prove it "independently" from the Deduction Theorem, but the proof is quite longer ...
The axioms are :
$F \rightarrow (G \rightarrow F)$
$(F \rightarrow (G \rightarrow H))\rightarrow ((F \rightarrow G) \rightarrow (F \rightarrow H))$
$(\neg G \rightarrow \neg F) \rightarrow ((\neg G \rightarrow F) \rightarrow G)$
For readibility, I'll organize the proof with some preliminary results :
T1 : $P \rightarrow P$
1) $P \rightarrow ((Q \rightarrow P) \rightarrow P)$ --- Ax.1
2) $P \rightarrow (Q \rightarrow P)$ --- Ax.1
3) $(1) \rightarrow ((2) \rightarrow (P \rightarrow P))$ --- Ax.2
4) $P \rightarrow P$ --- from 3), 1) and 2) by Modus Ponens twice.
T2 : $(Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$
1) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- Ax.2
2) $(1) \rightarrow ((Q \rightarrow R) \rightarrow (1))$ --- Ax.1
3) $(Q \rightarrow R) \rightarrow (1)$ --- from 1) and 2) by Modus Ponens
4) $(Q \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R))$ --- Ax.1
5) $(3) \rightarrow ((4) \rightarrow ((Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))))$ --- Ax.2
6) $(Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- from 5), 3) and 4) by MP twice.
T3 : $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$
1) $(P \rightarrow Q) \rightarrow (P \rightarrow Q)$ --- T1
2) $(1) \rightarrow (((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q))$ --- Ax.2
3) $((P \rightarrow Q) \rightarrow P) \rightarrow ((P \rightarrow Q) \rightarrow Q)$ --- from 1) and 2) by MP
4) $P \rightarrow ((P \rightarrow Q) \rightarrow P)$ --- Ax.1
5) $(3) \rightarrow ((4) \rightarrow (P \rightarrow ((P \rightarrow Q) \rightarrow Q)))$ --- T2
6) $P \rightarrow ((P \rightarrow Q) \rightarrow Q)$ --- from 5), 3) and 4) by MP twice.
T4 : $(P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))$
1) $((P \rightarrow Q) \rightarrow (P \rightarrow R)) \rightarrow ((Q \rightarrow (P \rightarrow Q)) \rightarrow (Q \rightarrow (P \rightarrow R)))$ --- T2
2) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$ --- Ax.2
3) $Q \rightarrow (P \rightarrow Q)$ --- Ax.1
4) $(1) \rightarrow ((2) \rightarrow ((P \rightarrow (Q \rightarrow R)) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R)))))$ --- T2
5) $(P \rightarrow (Q \rightarrow R)) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R)))$ --- from 4), 1) and 2) by MP twice
6) $(3) \rightarrow ((3) \rightarrow (Q \rightarrow (P \rightarrow R))) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- T3
7) $((3) \rightarrow (Q \rightarrow (P \rightarrow R))) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- from 6) and 3) by MP
8) $(7) \rightarrow ((5) \rightarrow ((P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))))$ --- T2
9) $(P \rightarrow (Q \rightarrow R)) \rightarrow (Q \rightarrow (P \rightarrow R))$ --- from 8), 7) and 5) by MP twice.
Now for the proof :
1) $(\neg C \rightarrow \neg B) \rightarrow ((\neg C \rightarrow B) \rightarrow C)$ --- Ax.3
2) $B \rightarrow (\neg C \rightarrow B)$ --- Ax.1
3) $(\neg C \rightarrow B) \rightarrow ((\neg C \rightarrow \neg B) \rightarrow C)$ --- from 1) and T4 by Modus Ponens
4) $B \rightarrow ((\neg C \rightarrow \neg B) \rightarrow C)$ --- from T2, 3) and 2) by MP twice
5) $(\neg C \rightarrow \neg B) \rightarrow (B \rightarrow C)$ --- from T4 and 4) by MP
You are right to suspect that your described method does not work to prove the Deduction Theorem: if you simply extend the existing deduction of $B$ from $\Delta \cup \{ A \}$ by adding $B \rightarrow (A \rightarrow B)$ (from axiom 1) and then getting $A \rightarrow B$ through Modus Ponens, then all you have ended up showing is that there is a deduction of $\Delta \cup \{ A\} \vdash A \rightarrow B$, because the original set of premises is still $\Delta \cup \{ A \}$. And you can't just throw out the $A$, since in the extended derivation, you still need to get to $B$ by itself, which may well depend on $A$.
So ... you need to do something else to show $\Delta \vdash A \rightarrow B$
Here is what you need to do. Transform the deduction of $\Delta \cup \{A \} \vdash B$ into a deduction of $\Delta \vdash A \rightarrow B$ by showing how you can get a deduction $\Delta \vdash A \rightarrow \varphi_i$ for $\varphi_i$ of the original deduction. And that you can show by strong induction, where you have to consider that every $\varphi_i$ comes about as one of the three cases: as an element of $\Delta$, an instance of some axiom, or by the use of Modus Ponens.
Here is a simple example:
If we take that $\Delta = \{ A \rightarrow B \}$, then we know that $\Delta \cup \{ A \} \vdash B$, i.e. that $\{ A \rightarrow B, A \} \vdash B$. Indeed, here is a derivation for that:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & A & Given\\
3 & B & \text{Modus Ponens } 2,3
\end{array}
OK, so now we want to convert this to a derivation of $\Delta \vdash A \rightarrow B$, i.e. of $\{ A \rightarrow B \} \vdash A \rightarrow B$
Now, there is of course a very simple derivation for $\{ A \rightarrow B \} \vdash A \rightarrow B$, but what I want to show below is that we can systematically convert the earlier derivation of $\{ A \rightarrow B, A \} \vdash B$ into a new derivation of $\{ A \rightarrow B \} \vdash A \rightarrow B$
Again, the basic idea is that, since we are 'pulling out' $A$ from the set of assumptions, in the new derivation we want to get a statement of the form $A \rightarrow \varphi_i$ for every line $\varphi_i$ from the original derivation. Think of this as 'conditionalizing' every statement with the condition $A$. So, the basic scheme for the derivation will look like:
\begin{array}{ccc}
..\\
k & A \rightarrow (A \rightarrow B) & ??\\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
Now, notice that the last line is $A \rightarrow B$, which is exactly what we are trying to get, so that's already good. But of course, we have yet to figure out how to actually get there. In fact, let's first enter the givens, which are all the same givens as in the original derivation, excvept for $A$, since that's the one we're 'pulling out':
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
..\\
k & A \rightarrow (A \rightarrow B) & ??\\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
OK, now, note that we put down line $k$ exactly because we had line $1$ as a given in the original derivation. That is, for tevery $\varphi_i \in \Delta$, we put down, and are trying to get to, $A \rightarrow \varphi_i$ .. how can we do that? Easy: just exploit axiom $1$:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
Now, the $A \rightarrow A$ is because the $A$ was in the original set of givens as well, but since in the new derivation we no longer have $A$ as a given, we need to derive $A \rightarrow A$ in a different way. But, as you found, such a derivation can always be done:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\
5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\
6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\
7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\
8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\
..\\
m & A \rightarrow B & ??
\end{array}
OK, almost done. Now we need to show how line $m$ can be derived from the original lines $k$ and $l$, i.e. lines $3$ and $8$. Well, for this you use axiom 2. That is, since in the original derivation we went from $A \rightarrow B$ and $A$ to $B$ via Modus Ponens, in the new derivation we need to do this using the conditionalized statements, i.e. we need to go from $A \rightarrow (A \rightarrow B)$ and $A \rightarrow A$ to $A \rightarrow B$. How do we do this? Well, this is exactly what Axiom 2 is for: Axiom 2 always looks a ittle weird if you first see it, but Axiom 2 is actually the embodiment of this kind of 'conditionalized Modus Ponens'. Here is how it goes:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\
5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\
6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\
7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\
8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\
9 & (A \rightarrow (A \rightarrow B))\rightarrow ((A \rightarrow A) \rightarrow (A \rightarrow B)) & \text{ Axiom } 2\\
10 & (A \rightarrow A) \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 3,9 \\
11 & A \rightarrow B & \text{ Modus Ponens } 8,10
\end{array}
.... and we're done!
OK, so this was just a simple example, but I think you can see how this general technique always works: Your goal is to conditionalize all statements from the original derivation with the '$A$' that you pull out, and you derive those as follows:
Derive $A \rightarrow A$ for that $A$.
Derive $A \rightarrow \varphi_i$ for every $\varphi_i \in \Delta$ using the $\varphi_i$ you still have as a given in the new derivation, and using axiom 1.
Derive any $A \rightarrow \varphi_k$ where in the original derivation $\varphi_k$ was derived using Modus Ponens from earlier $\varphi_i$ and $\varphi_j = \varphi_i \rightarrow \varphi_k$ from the conditionalized $A \rightarrow \varphi_i$ and $A \rightarrow \varphi_j = A \rightarrow (\varphi_i \rightarrow \varphi_k)$ using axiom 2
Best Answer
With the Deduction Theorem, you can do this:
$1. \alpha \to \beta \ (A.)$
$2. \neg \neg \alpha \ (A.)$
$3. \neg \neg \alpha \to \alpha \ (L5)$
$4. \alpha \ (MP \ 2,3)$
$5. \beta \ (MP 1,4)$
$6. \beta \to \neg \neg \beta \ (L6)$
$7. \neg \neg \beta \ (MP \ 5,6)$
So now we have shown $\alpha \to \beta, \neg \neg \alpha \vdash \neg \neg \beta$
With the Deduction Theorem, this means $\alpha \to \beta \vdash \neg \neg \alpha \to \neg \neg \beta$
Given $L3$, we have $\vdash (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha)$
And so we have $\alpha \to \beta \vdash \neg \beta \to \neg \alpha$
Applying the Deduction Theorem once more, we thus have $\vdash (\alpha \to \beta) \to (\neg \beta \to \neg \alpha)$
Note how this whole proof is a bit of a meta-proof: "Given that we can derive [this] from [that], and [such] from [so], we can also derive [bla] from [bloo]". In fact, anytime we rely on the Deduction Theorem, it becomes a meta-proof.
Now, all of that is perfectly acceptable as a mathematical proof of derivability, but it seems you would like to see this as more of a purely formal proof. That is, rather than a proof that something is derivable, you would like to see an actual formal derivation. How to do that?
Well, here is one way to do this. First, let's take the above meta-proof, and make it into what many people would call a Natural Deduction proof where you can make and discharge assumptions through the use of subproofs. Please note that actual Natural Deduction systems typically use $\to \ Elim$ and $\to \ Intro$ as rules, but I use MP and DT (Deduction Theorem) as justifications instead so you can see the clear connection with the meta-proof I did above:
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ \fitch{ 3. \neg \neg \alpha}{ 4. \neg \neg \alpha \to \alpha \qquad (L5)\\ 5. \alpha \qquad (MP \ 3,4)\\ 6. \beta \qquad (MP \ 2,5)\\ 7. \beta \to \neg \neg \beta \qquad (L6)\\ 8. \neg \neg \beta \qquad (MP \ 6,7) } \\ 9. \neg \neg \alpha \to \neg \neg \beta \qquad (DT \ 3-6)\\ 10. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 11. \neg \beta \to \neg \alpha \qquad (MP \ 9,10)\\}\\ 12. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad (DT \ 2-9)\\ }$
Next I will show you a systematic way of converting this natural deduction style proof into an axiom system style proof. The basic idea is to 'collapse' and get rid of the subproofs, and we'll do this in an inside-out manner. In fact, we'll do this through a process I call 'conditionalization'. Again, this process is a completely systematic process, and you should be able to to write a bit of computer code to do this.
OK, so the first thing we're going to do is to conditionalize the inner subproof. That is, note how lines 4 through 8 from this inner subproof are all dependent upon the assumption $\neg \neg \alpha$ on line 3. So we are going to take those lines, and make them the consequent of a conditional whose antecedent is that assumption $\neg \neg \alpha$.
In fact, we should conditionalize the assumption on line 3 itself. And since the resulting statement $\neg \neg \alpha \to \neg \neg \alpha$ is no longer an assumption of a subproof (since we're completely getting rid of that subproof), we'll have to show how we can actually infer that statement. Fortunately, we have axiom $L4$ to justify this in 1 step.
(Note: For any system that does not have axiom $L4$, please know that you can also derive this in 5 steps from axioms $L1 $and $L2$. Indeed, most axiom systems have axioms $L1$ and $L2$, and therefore do not have $L4$, as it is not really needed. Same goes for axiom $L5$ and $L6$ for that manner; your book or instructor has added those just for convenience, but in the professional literature there is no axiom system that uses all axioms 1 through 6, as axioms 1 through 3 already forms a comeplte system. And that system is known as the Lukasiewicz system, though some refer to it as the (or 'a' Hilbert system.)
As we conditionalize the statements on lines 4 through 8, the justifications for them are no longer valid. So for those statements too we'll need to show how we can derive them. However, the way they are derived currently will tell us exactly how to derive their conditionalized version, and I'll show how to do that later on. For now, let's change any Modus Ponens (MP) justification into a 'Conditionalized Modus Ponens' (C-MP), and we will justify any line that is a direct instantiation of an axiom with a 'Conditionalized Axiom' justification. So, for example, the conditionalization of line 7, which was originally an instantiation of $L6$, will now be justified using 'Conditionalized $L6$' (C-L6) instead. Below is the result of all this:
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. \neg \neg \alpha \to \neg \neg \alpha \qquad (L4)\\ 4. \neg \neg \alpha \to ( \neg \neg \alpha \to \alpha) \qquad (C-L5)\\ 5. \neg \neg \alpha \to \alpha \qquad (C-MP \ 3,4)\\ 6. \neg \neg \alpha \to \beta \qquad (C-MP \ 2,5)\\ 7. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (C-L6)\\ 8. \neg \neg \alpha \to \neg \neg \beta \qquad (C-MP \ 6,7)\\ 9. \neg \neg \alpha \to \neg \neg \beta \qquad (DT \ 3-8)\\ 10. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 11. \neg \beta \to \neg \alpha \qquad MP \ 9,10\\}\\ 12. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad \to Intro \ 2-9\\ }$
Now, a little more general house-keeping before I show how to do things like C-MP and C-L6:
Note how line 9 is a copy of line 8, so we can remove that now. On the other hand, we do want to conditionalize any statements that exist outside (before) the original subproof, but that were references inside the subproof that we are currently collapsing (think about it this way: when inside a subproof we make reference to a statement outside that subproof, we are in effect pulling that statement into the subproof (reiteration is what you would use to explicitly formalize that), and given that the conditionaliziation process is really conditionalizing the whole process that is going on inside a subproof, we need to conditionalize those referred statements as well. In this case: since we use line 2 in a MP on line 6, we'll need conditionalize it, and for that we can use axiom $L1$. So (updating line reference numbers as well):
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)\\ 4. \neg \neg \alpha \to (\alpha \to \beta) \qquad (MP \ 2,3)\\ 5. \neg \neg \alpha \to \neg \neg \alpha \qquad (L4)\\ 6. \neg \neg \alpha \to ( \neg \neg \alpha \to \alpha) \qquad (C-L5)\\ 7. \neg \neg \alpha \to \alpha \qquad (C-MP \ 5,6)\\ 8. \neg \neg \alpha \to \beta \qquad (C-MP \ 4,7)\\ 9. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (C-L6)\\ 10. \neg \neg \alpha \to \neg \neg \beta \qquad (C-MP \ 8,9)\\ 11. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 12. \neg \beta \to \neg \alpha \qquad (MP \ 10,11)\\}\\ 13. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad (DT \ 2-12)\\ }$
Also, just to avoid some unnecessary work, note that the only reason for lines 5 and 6 was to obtain line 7 ... but line 7 is an immediate application of axiom $L5$. So, we can simplify (if you ever write a program for the conversion process that I am going through here, you can make these kinds of simplifications optional, for they require some intelligence ... but without these simplifications, the conversion process is purely algorithmic):
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)\\ 4. \neg \neg \alpha \to (\alpha \to \beta) \qquad (MP \ 2,3)\\ 5. \neg \neg \alpha \to \alpha \qquad (L5)\\ 6. \neg \neg \alpha \to \beta \qquad (C-MP \ 4,5)\\ 7. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (C-L6)\\ 8. \neg \neg \alpha \to \neg \neg \beta \qquad (C-MP \ 6,7)\\ 9. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 10. \neg \beta \to \neg \alpha \qquad MP \ 8,9\\}\\ 11. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad \to Intro \ 2-10\\ }$
OK, but how are we going to obtain lines 6, 7, and 8? Well, there are basically two kinds of inferences we are doing: the conditionalized version of Modus Ponens (i.e. C-MP), or the conditionalization of an instance of some axiom (such as C-L6)
Let's first show how to do Conditionalized Modus Ponens, which will always look like this:
$1. \phi \to (\alpha \to \beta)$
$2. \phi \to \alpha$
$3. \phi \to \beta (C-MP \ 1,2)$
Well, the axiom $L2$ is ready made for this! In fact, this is of course not a conincidence, and is the very reason why most axiom systems contain axiom $L2$! OK, so we can just do:
$1. \phi \to (\alpha \to \beta)$
$2. \phi \to \alpha$
$3. (\phi \to (\alpha \to \beta)) \to ((\phi \to \alpha) \to (\phi \to \beta)) (L2)$
$4. (\phi \to \alpha) \to (\phi \to \beta) \qquad (MP \ 1,3)$
$5 \phi \to \beta \qquad (MP \ 2,4)$
Conditionalizing a single statement (such as the instance of an axiom) is even simpler, and for that we use the tailor-made axiom $L1$. For example, if we have statement $\psi$, and we want to conditionalize it with statement $phi$, we can simply do:
$1. \psi$
$2. \psi \to (\phi \to \psi) \qquad (L1)$
$3. \phi \to \psi \quad (MP \ 1,2)$
OK, so applying this process to lines 6,7, and 8, we get:
$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$
$\fitch{ 1.}{ \fitch{ 2. \alpha \to \beta}{ 3. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)\\ 4. \neg \neg \alpha \to (\alpha \to \beta) \qquad (MP \ 2,3)\\ 5. \neg \neg \alpha \to \alpha \qquad (L5)\\ 6. (\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)) \qquad (L2)\\ 7. (\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta) \qquad (MP \ 4,6)\\ 8. \neg \neg \alpha \to \beta \qquad (MP \ 5,7)\\ 9. \beta \to \neg \neg \beta \qquad (L6)\\ 10. (\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \qquad (L1)\\ 11. \neg \neg \alpha \to (\beta \to \neg \neg \beta) \qquad (MP \ 9,10)\\ 12. (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))) \qquad (L2)\\ 13. (\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \qquad (MP \ 11,12)\\ 14. \neg \neg \alpha \to \neg \neg \beta \qquad (MP \ 8,13)\\ 15. (\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)\\ 16. \neg \beta \to \neg \alpha \qquad (MP \ 14,15)\\}\\ 17. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad (DT \ 2-16)\\ }$
Phew! ... though that was only the first subproof conversion. Now we have to do the next subproof conversion. Since what we'll be doing here is really the same process as what we just did, I'll just show the result (the statements in blue are the conditionalizations of sentences 4 through 16 (as with the previous conversion, conditionalizing sentences 2 and 3 is unnecessary to get to 4):
$\color{blue}{1. (\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \qquad (L1)}$
$2. \neg \neg \alpha \to \alpha \qquad (L5)$
$3. (\neg \neg \alpha \to \alpha) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \alpha)) \qquad (L1)$
$\color{blue}{4. (\alpha \to \beta) \to (\neg \neg \alpha \to \alpha) \qquad (MP \ 2,3)}$
$5. (\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)) \qquad (L2)$
$6. ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)))) \qquad (L1)$
$\color{blue}{7. (\alpha \to \beta) \to ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \qquad (MP \ 5,6)}$
$8. ((\alpha \to \beta) \to ((\neg \neg \alpha \to (\alpha \to \beta)) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)))) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta)) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)))) \qquad (L2)$
$9. ((\alpha \to \beta) \to (\neg \neg \alpha \to (\alpha \to \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \qquad (MP \ 7,8)$
$\color{blue}{10. (\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta)) \qquad (MP \ 1,9)}$
$11.((\alpha \to \beta) \to ((\neg \neg \alpha \to \alpha) \to (\neg \neg \alpha \to \beta))) \to (((\alpha \to \beta) \to (\neg \neg \alpha \to \alpha)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \beta))) \qquad (L2)$
$12. ((\alpha \to \beta) \to (\neg \neg \alpha \to \alpha)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \beta)) \qquad (MP \ 10,11)$
$\color{blue}{13. (\alpha \to \beta) \to (\neg \neg \alpha \to \beta) \qquad (MP \ 4,12)}$
$14.\beta \to \neg \neg \beta \qquad (L6)$
$15.(\beta \to \neg \neg \beta) \to ((\alpha \to \beta) \to (\beta \to \neg \neg \beta)) \qquad (L1)$
$\color{blue}{16. (\alpha \to \beta) \to (\beta \to \neg \neg \beta) \qquad (MP \ 14,15)}$
$17.(\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \qquad (L1)$
$18.((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \to ((\alpha \to \beta) \to ((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)))) \qquad (L1)$
$\color{blue}{19. (\alpha \to \beta) \to ((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \qquad (MP \ 17,18)}$
$20.((\alpha \to \beta) \to ((\beta \to \neg \neg \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)))) \to (((\alpha \to \beta) \to (\beta \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)))) \qquad (L2)$
$21.((\alpha \to \beta) \to (\beta \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \qquad (MP \ 19,20)$
$\color{blue}{22. (\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \qquad (MP \ 16,21)}$
$23.(\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))) \qquad (L2)$
$24.((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))))) \qquad (L1)$
$\color{blue}{25. (\alpha \to \beta) \to ((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \qquad (MP \ 23,24)}$
$26.((\alpha \to \beta) \to ((\neg \neg \alpha \to (\beta \to \neg \neg \beta)) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))))) \to (((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))))) \qquad (L2)$
$27.((\alpha \to \beta) \to (\neg \neg \alpha \to (\beta \to \neg \neg \beta))) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \qquad (MP \ 25,26)$
$\color{blue}{28. (\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta))) \qquad MP \ 22,27}$
$29.((\alpha \to \beta) \to ((\neg \neg \alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)))) \to ((\neg \neg \alpha \to \neg \neg \beta) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \qquad (L2)$
$30.(\neg \neg \alpha \to \neg \neg \beta) \to ((\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta) \qquad (MP \ 28,29)$
$\color{blue}{31. (\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta) \qquad (MP \ 13,30)}$
$32.(\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) \qquad (L3)$
$33.((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha) ) \to ((\alpha \to \beta) \to ((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha))) \qquad (L1)$
$\color{blue}{34. (\alpha \to \beta) \to ((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha)) \qquad (MP \ 32, 33)}$
$35. ((\alpha \to \beta) \to ((\neg \neg \alpha \to \neg \neg \beta) \to (\neg \beta \to \neg \alpha))) \to (( (\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \beta \to \neg \alpha))) \qquad (L2) $
$36. ( (\alpha \to \beta) \to (\neg \neg \alpha \to \neg \neg \beta)) \to ((\alpha \to \beta) \to (\neg \beta \to \neg \alpha)) \qquad (MP \ 34,35)$
$\color{blue}{37. (\alpha \to \beta) \to (\neg \beta \to \neg \alpha) \qquad MP \ 31,36}$
OK! So what have we learned? That doing derivations in this system is not fun!! And that is why we use the Deduction Theorem to do a meta-proof of provability instead. And if you want the actual derivation, you can always systematically re-construct it from the meta-proof.