\begin{frame}
  \frametitle{MT and $\neg\neg_i$ as ``derived rules''}
  
  \begin{goal}{}
    The Modus Tollens rule derives \;$\neg \alpha$\; from \;$\alpha \to \beta$ and $\neg \beta$.
    \medskip\pause
    
    We can derive it using other rules as follows:
    \smallskip
    \begin{tikzpicture}
    \naturaldeduction{
      \mpause[1]{
        \proofstep{$\alpha \to \beta$}{premise};
      }
      \mpause{
        \proofstep{$\neg \beta$}{premise};
      }
      \mpause{
        \proofbox{
          \mpause{
            \proofstep{$\alpha$}{assumption};
          }
          \mpause{
            \proofstep{$\beta$}{$\to_e$ 3,1};
          }
          \mpause{
            \proofstep{$\bot$}{$\neg_e$ 2,4};
          }
        }
      }
      \mpause{
        \proofstep{$\neg \alpha$}{$\neg_i$ 3--5};
      }
    }
    \end{tikzpicture}
    \pause\pause\pause\pause\pause\pause\pause\pause
    \smallskip
    
    Thus: $\alpha \to \beta,\;\neg\beta \;\vdash \neg\alpha$\;.
  \end{goal}
  \pause
  
  \begin{block}{}
  This shows that $\neg\neg_i$ and MT are \emph{not needed},
  but sometimes help to make derivations easier or shorter.
  \end{block}
  
\end{frame}