183/183
\begin{frame}{Quantifier Operations (Advanced)}
  \begin{proposition}
    For all variables $\formula{\avarsynvar}$, and formulas $\aform$, $\bform$
    such that \alert{$\formula{\avarsynvar}$ does not occur free in $\bform$} it holds:  
    \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
      \item \; $\formula{\logimp{\forallst{\avarsynvar}{\aform}}{\bform}}
                \logequiv
                \formula{\existsst{\avarsynvar}{(\logimp{\aform}{\bform})}}$  
    \pause
      \item \; $\formula{\logimp{\existsst{\avarsynvar}{\aform}}{\bform}}
                \logequiv
                \formula{\forallst{\avarsynvar}{(\logimp{\aform}{\bform})}}$  
    \pause
      \item \; $\formula{(\logimp{\bform}{\existsst{\avarsynvar}{\aform}})}
                \logequiv
                \formula{\existsst{\avarsynvar}{(\logimp{\bform}{\aform})}}$  
    \pause
      \item \; $\formula{(\logimp{\bform}{\forallst{\avarsynvar}{\aform}})}
                \logequiv
                \formula{\forallst{\avarsynvar}{(\logimp{\bform}{\aform})}}$  
    \end{enumerate}  
  \end{proposition}  
\end{frame}