Theorem 19.29r2
Variation of 19.29r with double quantification. (Contributed by NM,
3-Feb-2005.)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \wedge \forall x \, \forall y \, \psi \rightarrow \exists x \, \exists y \, (\varphi \wedge \psi) \)
Proof
l0
19.29r
\( \vdash \exists x \, \exists y \, \varphi \wedge \forall x \, \forall y \, \psi \rightarrow \exists x \, (\exists y \, \varphi \wedge \forall y \, \psi) \)
19.29r
eximi _
\( \vdash \exists x \, (\exists y \, \varphi \wedge \forall y \, \psi) \rightarrow \exists x \, \exists y \, (\varphi \wedge \psi) \)
syl l0 _