16/179
\begin{frame}
  \frametitle{Rules for $\neg\neg$ and $\to$}
  
  \begin{goal}{Rules for $\neg\neg$}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\neg\neg_e}]
      {\phi}
      {\neg\neg\phi}
      &&
      \infer[\rulename{\neg\neg_i}]
      {\neg\neg\phi}
      {\phi}
    \end{align*}
  \end{goal}
  \pause\medskip

  \begin{goal}{Elimination rules for $\to$}
    This rule is called ``Modus Ponens'' (MP):
    \begin{align*}
      \infer[\rulename{\to_e} \;\; (or \rulename{MP})]
      {\psi}
      {\phi && \phi \to \psi}
    \end{align*}
    \pause
    This rule is called ``Modus Tollens'' (MT):
    \begin{align*}
      \infer[\rulename{MT}]
      {\neg\phi}
      {\phi \to \psi && \neg\psi}
    \end{align*}
  \end{goal}
\end{frame}