Theorem alinexa

A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)

Conclusion
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \leftrightarrow \neg \exists x \, (\varphi \wedge \psi) \)
Proof
l0
imnang
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \leftrightarrow \forall x \, \neg (\varphi \wedge \psi) \)
alnex
\( \vdash \forall x \, \neg (\varphi \wedge \psi) \leftrightarrow \neg \exists x \, (\varphi \wedge \psi) \)
bitri l0 _