Theorem exanali

A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)

Conclusion
\( \vdash \exists x \, (\varphi \wedge \neg \psi) \leftrightarrow \neg \forall x \, (\varphi \rightarrow \psi) \)
Proof
annim
l1
exbii _
\( \vdash \exists x \, (\varphi \wedge \neg \psi) \leftrightarrow \exists x \, \neg (\varphi \rightarrow \psi) \)
exnal
\( \vdash \exists x \, \neg (\varphi \rightarrow \psi) \leftrightarrow \neg \forall x \, (\varphi \rightarrow \psi) \)
bitri l1 _