Theorem alrimdv

Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 and 19.21v. (Contributed by NM, 10-Feb-1997.)

Hypothesis
alrimdv.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \chi \)
Proof
l0
ax-5
l1
ax-5
alrimdv.1
alrimdh l0 l1 _