Theorem alrimivv

Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 and 19.21v. (Contributed by NM, 31-Jul-1995.)

Hypothesis
alrimivv.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \forall y \, \psi \)
Proof
alrimivv.1
alrimiv _
alrimiv _