Theorem exrot4
Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, \varphi \leftrightarrow \exists z \, \exists w \, \exists x \, \exists y \, \varphi \)
Proof
excom13
l1
exbii _
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, \varphi \leftrightarrow \exists x \, \exists w \, \exists z \, \exists y \, \varphi \)
excom13
\( \vdash \exists x \, \exists w \, \exists z \, \exists y \, \varphi \leftrightarrow \exists z \, \exists w \, \exists x \, \exists y \, \varphi \)
bitri l1 _