Theorem eximi

Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)

Hypothesis
eximi.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \exists x \, \varphi \rightarrow \exists x \, \psi \)
Proof
l0
exim
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, \psi \)
eximi.1
\( \vdash \varphi \rightarrow \psi \)
mpg l0 _