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