Theorem exsimpl 1872

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

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

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

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

This theorem is referenced by:  19.40  1890  moexexlem  2628  elissetv  2819  clelab  2882  elex  3440  sbc5ALT  3740  r19.2zb  4423  dmcoss  5869  suppimacnvss  7960  unblem2  8997  kmlem8  9844  isssc  17449  krull  31545  bnj1143  32670  bnj1371  32909  bnj1374  32911  atex  37347  rtrclex  41114  clcnvlem  41120  pm10.55  41876