Theorem 2nalexn

Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)

Conclusion
\( \vdash \neg \forall x \, \forall y \, \varphi \leftrightarrow \exists x \, \exists y \, \neg \varphi \)
Proof
l0
df-ex
\( \vdash \exists x \, \exists y \, \neg \varphi \leftrightarrow \neg \forall x \, \neg \exists y \, \neg \varphi \)
alex
albii _
\( \vdash \forall x \, \forall y \, \varphi \leftrightarrow \forall x \, \neg \exists y \, \neg \varphi \)
xchbinxr l0 _
bicomi _