Theorem 19.40-2
Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris]
p. 90 with two quantifiers. (Contributed by Andrew Salmon,
24-May-2011.)
Conclusion
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \rightarrow \exists x \, \exists y \, \varphi \wedge \exists x \, \exists y \, \psi \)
Proof
19.40
l1
eximi _
\( \vdash \exists x \, \exists y \, (\varphi \wedge \psi) \rightarrow \exists x \, (\exists y \, \varphi \wedge \exists y \, \psi) \)
19.40
\( \vdash \exists x \, (\exists y \, \varphi \wedge \exists y \, \psi) \rightarrow \exists x \, \exists y \, \varphi \wedge \exists x \, \exists y \, \psi \)
syl l1 _