Theorem alrimd

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

Hypotheses
alrimd.1
\( \vdash \Finv x \, \varphi \)
alrimd.2
\( \vdash \Finv x \, \psi \)
alrimd.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \forall x \, \chi \)
Proof
l0
alrimd.1
alrimd.2
l2
a1i _
alrimd.3
alrimdd l0 l2 _