Theorem 2exbii

Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Hypothesis
2exbii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists x \, \exists y \, \psi \)
Proof
2exbii.1
exbii _
exbii _