Theorem sylg

A syllogism combined with generalization. Inference associated with sylgt. General form of alrimih. (Contributed by NM, 9-Jan-1993.) Extract from proof of alrimih. (Revised by BJ, 4-Oct-2019.)

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