Theorem 2ax5

Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)

Conclusion
\( \vdash \varphi \rightarrow \forall x \, \forall y \, \varphi \)
Proof
id
alrimivv _