Theorem 4exbidv

Formula-building rule for four existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995.)

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