Theorem exlimi

Inference associated with 19.23. See exlimiv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypotheses
exlimi.1
\( \vdash \Finv x \, \psi \)
exlimi.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \exists x \, \varphi \rightarrow \psi \)
Proof
exlimi.1
l1
19.23 _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, \varphi \rightarrow \psi \)
exlimi.2
\( \vdash \varphi \rightarrow \psi \)
mpgbi l1 _