Theorem exlimih

Inference associated with 19.23. See exlimiv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)

Hypotheses
exlimih.1
\( \vdash \psi \rightarrow \forall x \, \psi \)
exlimih.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \exists x \, \varphi \rightarrow \psi \)
Proof
exlimih.1
l1
nf5i _
exlimih.2
exlimi l1 _