Distribute a pair of existential quantifiers (over disjoint variables)
over a conjunction. Combination of 19.41v and 19.42v. For a
version with fewer disjoint variable conditions but requiring more
axioms, see eeanv. (Contributed by BJ, 30-Sep-2022.)
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \)
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
\( \vdash \exists x \, (\varphi \wedge \exists y \, \psi) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \)