Theorem ee4anv
Distribute two pairs of existential quantifiers over a conjunction. For
a version requiring fewer axioms but with additional disjoint variable
conditions, see 4exdistrv. (Contributed by NM, 31-Jul-1995.) Remove
disjoint variable conditions on y , z and x , w. (Revised by
Eric Schmidt, 26-Oct-2025.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \psi \)
Proof
excom
l1
exbii _
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists z \, \exists y \, \exists w \, (\varphi \wedge \psi) \)
eeanv
l3
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) \)
nfv
l5
nfex _
nfv
nfex _
eean l5 _
\( \vdash \exists x \, \exists z \, (\exists y \, \varphi \wedge \exists w \, \psi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \psi \)
3bitri l1 l3 _