Show $\vdash (\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi$. Note: $\lnot \phi$ is an abbreviation of $\phi \to \bot$. Using Dirk van Dalen. "Logic and Structure (Universitext)" as reference book.
Derivation:
$
\def\be{\mathsf{\tiny{\leftrightarrow} Elim}}
\def\bi{\mathsf{\tiny{\leftrightarrow} Intro}}
\def\ce{\mathsf{\tiny{\land} Elim}}
\def\ne#1{\mathsf{\tiny\neg Elim^{#1 }}}
\def\ni#1{\mathsf{\tiny\neg Intro^{#1}}}
\def\ii#1{\mathsf{\tiny{\to}Intro^{#1}}}
\def\ie{\mathsf{\tiny{\to}Elim}}
\def\RAA#1{\mathsf{\tiny RAA^{#1}}}
$
$
\dfrac{
  \dfrac{
      \dfrac{
        \dfrac{
          \dfrac{
            \dfrac{}{[\lnot \psi]_3}\dfrac{
              \dfrac{}{[\phi]_2}\dfrac{
                [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1
              }{\phi \to \psi}\ce
            }{\psi}\ie
          }{\bot}\ie
        }{\lnot \phi}\ni 2
      \dfrac{
        [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1
      }{\lnot \phi \to \psi}\ce
    }{\psi}\RAA 3 \dfrac{}{[\lnot \psi]_4}
  }{\psi}\ne 4
}{(\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi}\ii 1
$
My questions are:

*

*Is the hypotesis of $\lnot \psi$ labeled with a sub-index "4" correctly discharged ?

*Is this proof correct ?

EDIT:
Revised derivation:
$
\dfrac{
  \dfrac{
      \dfrac{
        \dfrac{
        \dfrac{
          \dfrac{
            \dfrac{}{[\lnot \psi]_3}\dfrac{
              \dfrac{}{[\phi]_2}\dfrac{
                [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1
              }{\phi \to \psi}\ce
            }{\psi}\ie
          }{\bot}\ie
        }{\lnot \phi}\ii 2
      \dfrac{
        [(\phi \to \psi) \land (\lnot \phi \to \psi)]_1
      }{\lnot \phi \to \psi}\ce
    }{\psi}\ie \dfrac{}{[\lnot \psi]_3}
      }{\bot}\ie
  }{\psi}\RAA 3
}{(\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi}\ii 1
$
 A: Your derivation up until $\neg \phi, \neg \phi \to \psi$ as well as the very last step are correct. Your idea that we need to get rid of the assumption $\neg \psi$ and for that purpose provoke a contradiction in order to then apply $RAA$ thereby discharging the assumption is also correct, but you got the rules a bit mixed up there.
The next step which combines $\neg \phi$ and $\neg \phi \to \psi$ to yield $\psi$ is not RAA, but $\to Elim$. This rule does not allow to discharge assumptions and we still need to get rid of the assumption $\neg \psi$. So even though we already established the desired conclusion $\psi$, we need to make a detour with further steps in order to kill the remaining assumption along the way.
Performing a $\neg Elim$ with assumption $\neg \psi$ first leads to $\bot$. From that you can then conclude $\psi$ by an application of $RAA$, thereby discharging both occurrences of the assumption $\neg \psi$ (the one that was still open from earlier and the one we just opened).
This allows you to then complete the proof with $\to Intro$.
[-psi]3
  ...            ...
 -phi        -phi -> psi
------------------------- (-> E)
           psi                     [-psi]3
          ------------------------------ (- E)
                        ⊥
                       --- (RAA)3
                       psi            
     ------------------------------------- (-> I)1
      (phi -> psi) ^ (-phi -> psi) -> psi

These are two common patterns in ND proofs that are "difficult":

*

*We already established some desired formula but still got open assumptions to deal with, so we apply a couple extra steps ending up with the same formula but killing some assumptions along the way.

*We open the same assumption at different points in the proof, and eventually discharge all occurrences in the same step.

A: Using quite another proof system -- apologies -- but this may help...

