Theorem alrimih

Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 and 19.21h. Instance of sylg. (Contributed by NM, 9-Jan-1993.)

Hypotheses
alrimih.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
alrimih.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \forall x \, \psi \)
Proof
l0
alrimih.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
alrimih.2
\( \vdash \varphi \rightarrow \psi \)
sylg l0 _