Theorem exsimpr

Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Conclusion
\( \vdash \exists x \, (\varphi \wedge \psi) \rightarrow \exists x \, \psi \)
Proof
simpr
eximi _