Theorem 4exdistr
Distribution of existential quantifiers in a quadruple conjunction.
(Contributed by NM, 9-Mar-1995.) (Proof shortened by Wolf Lammen,
20-Jan-2018.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, (\varphi \wedge \psi \wedge (\chi \wedge \theta)) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, (\psi \wedge \exists z \, (\chi \wedge \exists w \, \theta))) \)
Proof
19.42v
l1
anbi2i _
\( \vdash \varphi \wedge \psi \wedge \exists w \, (\chi \wedge \theta) \leftrightarrow \varphi \wedge \psi \wedge (\chi \wedge \exists w \, \theta) \)
l2
19.42v
\( \vdash \exists w \, (\varphi \wedge \psi \wedge (\chi \wedge \theta)) \leftrightarrow \varphi \wedge \psi \wedge \exists w \, (\chi \wedge \theta) \)
df-3an
\( \vdash \varphi \wedge \psi \wedge \chi \wedge \exists w \, \theta \leftrightarrow \varphi \wedge \psi \wedge (\chi \wedge \exists w \, \theta) \)
3bitr4i l1 l2 _
l5
3exbii _
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, (\varphi \wedge \psi \wedge (\chi \wedge \theta)) \leftrightarrow \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi \wedge \chi \wedge \exists w \, \theta) \)
3exdistr
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi \wedge \chi \wedge \exists w \, \theta) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, (\psi \wedge \exists z \, (\chi \wedge \exists w \, \theta))) \)
bitri l5 _