\begin{frame}[t]
  \frametitle{Logical Equivalence, and Validity of Bi-implication}  

  \begin{proposition}
    For all formulas $\aform$, $\bform$ the following statements are equivalent:
    \begin{enumerate}[(i)]
      \item $\aform \logequiv \bform$
      \item $\formula{\aform \logbiimpinf \bform}$ is valid.
    \end{enumerate}
  \end{proposition}
  \pause
  
  \begin{proof}
    For all models $\model{\amodel}$ and environments $\saluf$ it holds:
    \begin{talign}
      & \model{\amodel} \satisfieslookup{\saluf} \formula{\logbiimp{\aform}{\bform}} \\
      & \;\;\Longleftrightarrow\;\;
        \model{\amodel} \satisfieslookup{\saluf} \formula{\logand{(\logimp{\aform}{\bform})}{(\logimp{\bform}{\aform})}} \\
      & \;\;\Longleftrightarrow\;\;
        \model{\amodel} \satisfieslookup{\saluf} \formula{\logimp{\aform}{\bform}}
        \;\text{ and }\;
        \model{\amodel} \satisfieslookup{\saluf} \formula{\logimp{\bform}{\aform}} \\
      & \;\;\Longleftrightarrow\;\; \hphantom{\;\;\text{and}\;}
        \text{if } \model{\amodel} \satisfieslookup{\saluf} \aform\,,
        \text{ then } \model{\amodel} \satisfieslookup{\saluf} \bform, \\
      & \hphantom{\;\;\Longleftrightarrow\;\;} \;\;\text{and}\;\;\;
        \text{if } \model{\amodel} \satisfieslookup{\saluf} \bform\,,
        \text{ then } \model{\amodel} \satisfieslookup{\saluf} \aform \\
      & \;\;\Longleftrightarrow\;\;
        (\model{\amodel} \satisfieslookup{\saluf} \aform
         \;\Longleftrightarrow\;
         \model{\amodel} \satisfieslookup{\saluf} \bform)
    \end{talign}
    From this we conclude: 
    $\formula{\aform \logbiimpinf \bform}$ is valid if and only if $\aform \logequiv \bform$.
  \end{proof}
  \vspace{10cm}
\end{frame}