Theorem alrimiv

Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 and 19.21v. (Contributed by NM, 21-Jun-1993.)

Hypothesis
alrimiv.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \psi \)
Proof
l0
ax-5
alrimiv.1
alrimih l0 _