\begin{frame}{Quantifier Operations}
  
  \begin{proposition}
  For all variables $\formula{\avarsynvar}$, $\formula{\bvarsynvar}$ and formulas $\aform$ it holds:  
  \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
    \item \; $\formula{{\forallst{\avarsynvar}{\forallst{\bvarsynvar}{\,\aform}}}}
              \logequiv
              \formula{{\forallst{\bvarsynvar}{\forallst{\avarsynvar}{\,\aform}}}}$
  \pause
    \item \; $\formula{{\existsst{\avarsynvar}{\existsst{\bvarsynvar}{\,\aform}}}}
              \logequiv
              \formula{{\existsst{\bvarsynvar}{\existsst{\avarsynvar}{\,\aform}}}}$ 
  \pause
    \item \; $\formula{\forallst{\avarsynvar}{\,\aform}} \logequiv \aform$
      \hspace*{0.5ex} if $\avarsynvar$ not free in $\aform$   
  \pause
    \item \; $\formula{\existsst{\avarsynvar}{\,\aform}} \logequiv \aform$
      \hspace*{0.5ex} if $\avarsynvar$ not free in $\aform$
  \end{enumerate}  
  \end{proposition}  
  \pause\bigskip
  
  \begin{alertblock}{}
    However, \alert{in general}:
    \begin{talign}
      \formula{{\existsst{\avarsynvar}{\forallst{\bvarsynvar}{\,\aform}}}}
      \lognotequiv
      \formula{{\forallst{\bvarsynvar}{\existsst{\avarsynvar}{\,\aform}}}}
    \end{talign}
  \end{alertblock}
\end{frame}