\begin{frame} \frametitle{Introduction of $\to$} \begin{goal}{Introduction rule for $\to$} \vspace{-1ex} \begin{align*} \infer[\rulename{\to_i}] {\alpha \to \beta} { \framebox{\parbox{.8cm}{\centerline{$\alpha$}\centerline{$\vdots$}\centerline{$\beta$}}} } \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}