Theorem exsimpl 1869

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 207  df-an 396  df-ex 1781

This theorem is referenced by:  19.40  1887  moexexlem  2621  elissetv  2812  clelab  2876  elexOLD  3458  sbc5ALT  3770  r19.2zb  4446  dmcoss  5914  dmcossOLD  5915  suppimacnvss  8103  unblem2  9177  kmlem8  10049  isssc  17727  krull  33442  bnj1143  34800  bnj1371  35039  bnj1374  35041  atex  39451  rtrclex  43656  clcnvlem  43662  pm10.55  44408