Theorem 2exanali

Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)

Conclusion
\( \vdash \neg \exists x \, \exists y \, (\varphi \wedge \neg \psi) \leftrightarrow \forall x \, \forall y \, (\varphi \rightarrow \psi) \)
Proof
2nalexn
l1
con1bii _
\( \vdash \neg \exists x \, \exists y \, \neg (\varphi \rightarrow \psi) \leftrightarrow \forall x \, \forall y \, (\varphi \rightarrow \psi) \)
annim
2exbii _
\( \vdash \exists x \, \exists y \, (\varphi \wedge \neg \psi) \leftrightarrow \exists x \, \exists y \, \neg (\varphi \rightarrow \psi) \)
xchnxbir l1 _