How do I derive a proper natural deduction proof for $\{(\phi\leftrightarrow(\psi\leftrightarrow\psi))\}\vdash\phi$?

Question

I tried to derive a natural deduction proof for the sequent as below, but it feels wrong.

Below is the latex code. How should I prove this correctly?

\documentclass[oneside,12pt]{article}

\usepackage[a4paper]{geometry}
\usepackage{microtype}
\usepackage[T1]{fontenc}
\usepackage{enumitem}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{ebproof}
\usepackage{cancel}

% section
\setcounter{section}{2}
\setcounter{subsection}{5}
% enumerate
\setlist[enumerate,1]{label=\thesubsection.\arabic*.}
% theorems
\newtheorem*{thm}{Theorem}
\newtheorem*{lem}{Lemma}
\theoremstyle{definition}
\newtheorem*{sol}{Solution}
% ebproof
\ebproofset{left label template=$\inserttext$,right label template=$\inserttext$}

\newcommand{\mathcircled}[1]{\mbox{\textcircled{\scriptsize #1}}}
\newcommand{\ra}{\rightarrow}
\newcommand{\lra}{\leftrightarrow}

\begin{document}
\begin{enumerate}
\item Give derivations to prove the following sequents:
  \begin{enumerate}
    \setcounter{enumii}{4}
  \item $\{(\phi\lra(\psi\lra\psi))\}\vdash\phi$
    \begin{sol}
      \[
        \begin{prooftree}
          \Hypo{\bcancel{\phi}}
          \Hypo{(\phi\lra(\psi\lra\psi))}
          \Infer1[(\lra E)]{(\phi\ra(\psi\lra\psi))}
          \Infer2[(\ra E)]{(\psi\lra\psi)}
          \Hypo{(\phi\lra(\psi\lra\psi))}
          \Infer1[(\lra E)]{((\psi\lra\psi)\ra\phi)}
          \Infer2[(\ra E)]{\phi}
        \end{prooftree}
      \]
    \end{sol}
  \end{enumerate}
\end{enumerate}
\end{document}

Answer 1

I solved it by myself. Solving problems is fun.