Theorem alrimi

Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses
alrimi.1
\( \vdash \Finv x \, \varphi \)
alrimi.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \psi \)
Proof
alrimi.1
l1
nf5ri _
alrimi.2
alrimih l1 _