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 1837	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  19.40  1888  moexexlem  2627  elissetv  2818  clelab  2881  elexOLD  3464  sbc5ALT  3771  dmcoss  5932  dmcossOLD  5933  suppimacnvss  8125  unblem2  9205  kmlem8  10080  isssc  17756  krull  33571  bnj1143  34965  bnj1371  35204  bnj1374  35206  atex  39779  rtrclex  43970  clcnvlem  43976  pm10.55  44722