\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}