Theorem 3exdistr
Distribution of existential quantifiers in a triple conjunction.
(Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon,
25-May-2011.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, (\psi \wedge \exists z \, \chi)) \)
Proof
3anass
l1
2exbii _
\( \vdash \exists y \, \exists z \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \exists y \, \exists z \, (\varphi \wedge (\psi \wedge \chi)) \)
l2
19.42vv
\( \vdash \exists y \, \exists z \, (\varphi \wedge (\psi \wedge \chi)) \leftrightarrow \varphi \wedge \exists y \, \exists z \, (\psi \wedge \chi) \)
exdistr
anbi2i _
\( \vdash \varphi \wedge \exists y \, \exists z \, (\psi \wedge \chi) \leftrightarrow \varphi \wedge \exists y \, (\psi \wedge \exists z \, \chi) \)
3bitri l1 l2 _
exbii _