Theorem eeeanv
Distribute three existential quantifiers over a conjunction.
(Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon,
25-May-2011.) Reduce distinct variable restrictions. (Revised by Wolf
Lammen, 20-Jan-2018.)
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
eeanv
l1
anbi1i _
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \wedge \exists z \, \chi \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \wedge \exists z \, \chi \)
df-3an
l3
exbii _
\( \vdash \exists z \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \exists z \, (\varphi \wedge \psi \wedge \chi) \)
19.42v
\( \vdash \exists z \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \wedge \exists z \, \chi \)
bitri l3 _
l6
2exbii _
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \exists x \, \exists y \, (\varphi \wedge \psi \wedge \exists z \, \chi) \)
nfv
nfex _
19.41 _
l10
exbii _
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi \wedge \exists z \, \chi) \leftrightarrow \exists x \, (\exists y \, (\varphi \wedge \psi) \wedge \exists z \, \chi) \)
nfv
nfex _
19.41 _
\( \vdash \exists x \, (\exists y \, (\varphi \wedge \psi) \wedge \exists z \, \chi) \leftrightarrow \exists x \, \exists y \, (\varphi \wedge \psi) \wedge \exists z \, \chi \)
l14
3bitri l6 l10 _
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi \wedge \chi) \leftrightarrow \exists x \, \exists y \, (\varphi \wedge \psi) \wedge \exists z \, \chi \)
df-3an
\( \vdash \exists x \, \varphi \wedge \exists y \, \psi \wedge \exists z \, \chi \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \wedge \exists z \, \chi \)
3bitr4i l1 l14 _