32/179
\begin{frame}
  \frametitle{Introduction of $\to$}
  
  \begin{goal}{Introduction rule for $\to$}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\to_i}]
      {\phi \to \psi}
      {
        \framebox{\parbox{.8cm}{\centerline{$\phi$}\centerline{$\vdots$}\centerline{$\psi$}}}
      }
    \end{align*}
  \end{goal}
  \pause
  
  \begin{exampleblock}{}
    Derivation of \quad $p \to q \;\vdash\; \neg q \to \neg p$:
    \pause\medskip
    
    \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$p \to q$}{premise};   
      \mpause[1]{
        \proofbox{
          \mpause{
            \proofstep{$\neg q$}{assumption};
          }
          \mpause{
            \proofstep{$\neg p$}{MT 1,2};
          }
        }
      }
      \mpause{
        \proofstep{$\neg q \to \neg p$}{$\to_i$ 2--3};
      }
    }
    \end{tikzpicture}
  \end{exampleblock}
\end{frame}