Theorem eximii

Inference associated with eximi. (Contributed by BJ, 3-Feb-2018.)

Hypotheses
eximii.1
\( \vdash \exists x \, \varphi \)
eximii.2
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \exists x \, \psi \)
Proof
l0
eximii.1
\( \vdash \exists x \, \varphi \)
eximii.2
eximi _
\( \vdash \exists x \, \varphi \rightarrow \exists x \, \psi \)
ax-mp l0 _