Theorem
exdistr2
Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, \exists z \, \psi) \)
Proof
19.42vv
exbii
_
This is the content in the right pane.