In P.D. Magnus. forallX: an Introduction to Formal Logic (p. 174, exercise D), appears this exercise:
D. Show that if you had LEM as a basic rule, you could justify IP as a derived rule. That is, suppose you had the proof: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\ei#1{\qquad\mathbf{\exists I} \: #1 \\} $ $$ \fitch{}{ \fitch{\neg A}{ \ldots\\ \bot } } $$
How could you use it to prove A without using IP but with using LEM as well as all the other basic rules?
I tried to prove it in this manner:
$ \fitch{}{ \fitch{1. \ \neg A}{ \ldots\\ k. \bot \\ }\\ \fitch{k+1.\ A}{ A \R{k + 1} }\\ \fitch{k+2. \ \neg A}{ \bot\\ A } } $
Am I approaching what is requested in a proper manner ?
$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}$
Yes.
You have used Explosion (ex falso quodlibet.) and now need to use LEM and disjunction elimination.
Also if you do not wish to combine the first and third proof into one, then you need to add a conditional introduction so that you can validly justify deriving $\bot$ from the second assumed $\neg A$ (with conditional elimination).
(Plus, you do not technically need to reiterate the assumption in the second subproof, but some proof checkers may require it.)
$$\fitch{}{\fitch{~~~~~1.~~\neg A}{~~~~~~~\vdots\\~~~~~k.~~\bot}\\k{+}1.~~ \neg A\to\bot\hspace{4ex}{\to}\mathsf I~1{-}(k)\\\fitch{k{+}2.~~A\hspace{8ex}}{k{+}3.~~A\hspace{8ex}\mathsf R~(k{+}2)}\\\fitch{k{+}4.~~\neg A\hspace{6.5ex}}{k{+}5.~~\bot\hspace{7.5ex}{\to}\mathsf E~(k{+}4), (k{+}1)\\k{+}6.~~A\hspace{8ex}\mathsf X~(k{+}5)}\\k{+}7.~~A\vee\neg A\hspace{5ex}\textsf{LEM}\\k{+}8.~~A\hspace{11ex}{\vee}\mathsf E~(k{+}7),(k{+}2){-}(k{+}3),(k{+}4){-}(k{+}6)}$$