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