\begin{frame}
  \frametitle{Derivation with Natural Deduction}
  
  \begin{exampleblock}{}
  Can we derive \quad$\neg r \to \neg q$\quad from \quad$p \to (q \to r),\; p$\quad? 
  \pause\medskip
  
  \begin{tikzpicture}
  \naturaldeduction{
    \proofstep{$p \to (q \to r)$}{premise};   
    \mpause[1]{
    \proofstep{$p$}{premise};   
    }
    \mpause{
      \proofbox{
        \mpause{
        \proofstep{$\neg r$}{assumption};
        }
        \mpause{
        \proofstep{$q \to r$}{$\to_e$ 2,1};
        }
        \mpause{
        \proofstep{$\neg q$}{MT 4,3};
        }
      }
    }
    \mpause{
      \proofstep{$\neg r \to \neg q$}{$\to_i$ 3--5};
    }
  }
  \end{tikzpicture}
  \pause\pause\pause\pause\pause\pause\pause
  \medskip
  
  Hence we have derived
  \begin{talign}
    p \to (q \to r),\; p \quad\vdash\quad \neg r \to \neg q
  \end{talign}
  \end{exampleblock}
\end{frame}