Theorem exsimpl 1870

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

Assertion

Ref	Expression
exsimpl	⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)

Proof of Theorem exsimpl

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	eximi 1836	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781

This theorem is referenced by:  19.40  1888  moexexlem  2621  elissetv  2813  clelab  2878  elex  3492  sbc5ALT  3806  r19.2zb  4495  dmcoss  5970  suppimacnvss  8163  unblem2  9302  kmlem8  10158  isssc  17774  krull  33033  bnj1143  34264  bnj1371  34503  bnj1374  34505  atex  38740  rtrclex  42830  clcnvlem  42836  pm10.55  43590