Theorem exsimpl

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 \, \varphi \)

Proof

simpl

eximi _