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  2623  elissetv  2814  clelab  2877  elexOLD  3459  sbc5ALT  3766  dmcoss  5920  dmcossOLD  5921  suppimacnvss  8111  unblem2  9186  kmlem8  10058  isssc  17731  krull  33453  bnj1143  34825  bnj1371  35064  bnj1374  35066  atex  39528  rtrclex  43737  clcnvlem  43743  pm10.55  44489