Theorem 4exdistrv

Distribute two pairs of existential quantifiers (over disjoint variables) over a conjunction. For a version with fewer disjoint variable conditions but requiring more axioms, see ee4anv. (Contributed by BJ, 5-Jan-2023.)

Conclusion
\( \vdash \exists x \, \exists z \, \exists y \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \psi \)
Proof
exdistrv
l1
2exbii _
\( \vdash \exists x \, \exists z \, \exists y \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists z \, (\exists y \, \varphi \wedge \exists w \, \psi) \)
exdistrv
\( \vdash \exists x \, \exists z \, (\exists y \, \varphi \wedge \exists w \, \psi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \psi \)
bitri l1 _