Theorem exlimiiv

Inference (Rule C) associated with exlimiv. (Contributed by BJ, 19-Dec-2020.)

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