Theorem 2albidv

Formula-building rule for two universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.)

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