Theorem exlimdh

Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.)

Hypotheses
exlimdh.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
exlimdh.2
\( \vdash \chi \rightarrow \forall x \, \chi \)
exlimdh.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \psi \rightarrow \chi \)
Proof
exlimdh.1
l1
nf5i _
exlimdh.2
l3
nf5i _
exlimdh.3
exlimd l1 l3 _