Theorem alimi

Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)

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