Theorem 19.42vvv

Version of 19.42 with three quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Sep-2011.) (Proof shortened by Wolf Lammen, 27-Aug-2023.)

Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \varphi \wedge \exists x \, \exists y \, \exists z \, \psi \)
Proof
l0
exdistr2
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, \exists z \, \psi) \)
19.42v
\( \vdash \exists x \, (\varphi \wedge \exists y \, \exists z \, \psi) \leftrightarrow \varphi \wedge \exists x \, \exists y \, \exists z \, \psi \)
bitri l0 _