Theorem 3exbidv

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

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