Theorem exan

Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof shortened by Wolf Lammen, 6-Nov-2022.) Expand hypothesis. (Revised by Steven Nguyen, 19-Jun-2023.)

Hypotheses
exan.1
\( \vdash \exists x \, \varphi \)
exan.2
\( \vdash \psi \)
Conclusion
\( \vdash \exists x \, (\varphi \wedge \psi) \)
Proof
l0
exan.1
\( \vdash \exists x \, \varphi \)
exan.2
jctr _
\( \vdash \varphi \rightarrow \varphi \wedge \psi \)
eximii l0 _