Theorem 19.21bbi

Inference removing two universal quantifiers. Version of 19.21bi with two quantifiers. (Contributed by NM, 20-Apr-1994.)

Hypothesis
19.21bbi.1
\( \vdash \varphi \rightarrow \forall x \, \forall y \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
19.21bbi.1
\( \vdash \varphi \rightarrow \forall x \, \forall y \, \psi \)
19.21bi _
\( \vdash \varphi \rightarrow \forall y \, \psi \)
19.21bi _