Theorem 2exbidv

Formula-building rule for two existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)

Hypothesis
2albidv.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\exists x \, \exists y \, \psi \leftrightarrow \exists x \, \exists y \, \chi) \)
Proof
2albidv.1
exbidv _
exbidv _