An equivalence between an implication with an existentially quantified
antecedent and an implication with a universally quantified consequent.
An interesting case is when the same formula is substituted for both
\( \varphi \) and \( \psi \), since then both implications express a type of
nonfreeness. See also alimex. (Contributed by BJ, 12-May-2019.)
\( \vdash \exists x \, \varphi \rightarrow \psi \leftrightarrow \neg \psi \rightarrow \forall x \, \neg \varphi \)
\( \vdash \exists x \, \varphi \rightarrow \psi \leftrightarrow \neg \forall x \, \neg \varphi \rightarrow \psi \)
\( \vdash \neg \forall x \, \neg \varphi \rightarrow \psi \leftrightarrow \neg \psi \rightarrow \forall x \, \neg \varphi \)