Theorem excom13
Swap 1st and 3rd existential quantifiers. (Contributed by NM,
9-Mar-1995.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \varphi \leftrightarrow \exists z \, \exists y \, \exists x \, \varphi \)
Proof
l0
excom
\( \vdash \exists x \, \exists y \, \exists z \, \varphi \leftrightarrow \exists y \, \exists x \, \exists z \, \varphi \)
excom
l2
exbii _
\( \vdash \exists y \, \exists x \, \exists z \, \varphi \leftrightarrow \exists y \, \exists z \, \exists x \, \varphi \)
excom
\( \vdash \exists y \, \exists z \, \exists x \, \varphi \leftrightarrow \exists z \, \exists y \, \exists x \, \varphi \)
3bitri l0 l2 _