Theorem ee4anvOLD
Obsolete version of ee4anv as of 26-Oct-2025. (Contributed by NM,
31-Jul-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \psi \)
Proof
excom
l1
exbii _
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists z \, \exists y \, \exists w \, (\varphi \wedge \psi) \)
eeanv
l3
2exbii _
\( \vdash \exists x \, \exists z \, \exists y \, \exists w \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \exists z \, (\exists y \, \varphi \wedge \exists w \, \psi) \)
eeanv
\( \vdash \exists x \, \exists z \, (\exists y \, \varphi \wedge \exists w \, \psi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \psi \)
3bitri l1 l3 _