\begin{frame}[t]{Logical Equivalence}
  
  \renewcommand{\slogequiv}{\textcolor{firebrick}{\equiv}}
  
  \begin{block}{Theorem}
    \begin{malign}
      \aform \logequiv \bform \;\;\;\iff\;\;\;
      \aform \satisfies \bform
      \;\text{ and }\;
      \bform \satisfies \aform
    \end{malign}
  \end{block}

  Therefore, logical equivalence is sometimes denoted $\mathrel{\reflectbox{$\ssatisfies$}}\satisfies$.
  \bigskip

  \begin{proof}
    \begin{malign}
      & \aform \logequiv \bform \\
      & \;\;\iff\;\; \text{for all $\model{\amodel}$ and $\saluf\,$:} \\[-0.75ex]
      & \phantom{\;\;\iff\;\;} \;\,
        (\model{\amodel} \satisfieslookup{\saluf} \aform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \bform)
        \text{ and }
        (\model{\amodel} \satisfieslookup{\saluf} \bform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \aform) \\
      & \;\;\iff\;\; \text{for all $\model{\amodel}$ and $\saluf\,$:} \;\;
        \model{\amodel} \satisfieslookup{\saluf} \aform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \bform) \\[-0.75ex] 
      & \phantom{\;\;\iff\;\;} \;\, \text{and for all $\model{\amodel}$ and $\saluf\,$:} \;\;
        \model{\amodel} \satisfieslookup{\saluf} \bform \;\Rightarrow\; \model{\amodel} \satisfieslookup{\saluf} \aform) \\
      & \;\;\iff\;\; \aform \satisfies \bform \;\;\text{and}\;\; \bform \satisfies \aform \;\;  
        \text{(that is, $\aform \:\mathrel{\reflectbox{$\ssatisfies$}}\satisfies\: \bform$)}
    \end{malign}
  \end{proof}  
\end{frame}