Theorem exrot3
Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \varphi \leftrightarrow \exists y \, \exists z \, \exists x \, \varphi \)
Proof
l0
excom13
\( \vdash \exists x \, \exists y \, \exists z \, \varphi \leftrightarrow \exists z \, \exists y \, \exists x \, \varphi \)
excom
\( \vdash \exists z \, \exists y \, \exists x \, \varphi \leftrightarrow \exists y \, \exists z \, \exists x \, \varphi \)
bitri l0 _