Theorem 2eximi

Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis
eximi.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \rightarrow \exists x \, \exists y \, \psi \)
Proof
eximi.1
eximi _
eximi _