Theorem exsimpl 1875

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 483	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	eximi 1841	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787

This theorem is referenced by:  19.40  1893  moexexlem  2630  elissetv  2821  clelab  2885  elex  3449  sbc5ALT  3749  r19.2zb  4432  dmcoss  5879  suppimacnvss  7980  unblem2  9045  kmlem8  9914  isssc  17530  krull  31639  bnj1143  32766  bnj1371  33005  bnj1374  33007  atex  37416  rtrclex  41195  clcnvlem  41201  pm10.55  41957