Theorem eean
Distribute existential quantifiers. (Contributed by NM, 27-Oct-2010.)
(Revised by Mario Carneiro, 6-Oct-2016.)
Hypotheses
eean.1
\( \vdash \Finv y \, \varphi \)
eean.2
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \)
Proof
eean.1
19.42 _
l2
exbii _
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\varphi \wedge \exists y \, \psi) \)
eean.2
nfex _
19.41 _
\( \vdash \exists x \, (\varphi \wedge \exists y \, \psi) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \psi \)
bitri l2 _