Theorem 19.41vvvv
Version of 19.41 with four quantifiers and a disjoint variable
condition requiring fewer axioms. (Contributed by FL, 14-Jul-2007.)
Conclusion
\( \vdash \exists w \, \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \exists w \, \exists x \, \exists y \, \exists z \, \varphi \wedge \psi \)
Proof
19.41vvv
l1
exbii _
\( \vdash \exists w \, \exists x \, \exists y \, \exists z \, (\varphi \wedge \psi) \leftrightarrow \exists w \, (\exists x \, \exists y \, \exists z \, \varphi \wedge \psi) \)
19.41v
\( \vdash \exists w \, (\exists x \, \exists y \, \exists z \, \varphi \wedge \psi) \leftrightarrow \exists w \, \exists x \, \exists y \, \exists z \, \varphi \wedge \psi \)
bitri l1 _