Theorem exsimpl 1868

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

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

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

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

This theorem is referenced by:  19.40  1886  moexexlem  2625  elissetv  2815  clelab  2880  elexOLD  3481  sbc5ALT  3794  r19.2zb  4471  dmcoss  5954  suppimacnvss  8172  unblem2  9301  kmlem8  10172  isssc  17833  krull  33494  bnj1143  34821  bnj1371  35060  bnj1374  35062  atex  39425  rtrclex  43641  clcnvlem  43647  pm10.55  44393