Theorem 3exbii

Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)

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