Theorem exdistr

Distribution of existential quantifiers. See also exdistrv. (Contributed by NM, 9-Mar-1995.)

Conclusion
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
Proof
19.42v
exbii _