Theorem 2alimi

Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

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