Theorem 19.41vvv
Version of 19.41 with three quantifiers and a disjoint variable
condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists y \, \exists z \, \varphi \wedge \psi \)
Proof
19.41vv
l1
exbii _
\( \vdash \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\exists y \, \exists z \, \varphi \wedge \psi) \)
19.41v
\( \vdash \exists x \, (\exists y \, \exists z \, \varphi \wedge \psi) \leftrightarrow \exists x \, \exists y \, \exists z \, \varphi \wedge \psi \)
bitri l1 _