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 1842	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 208  df-an 397  df-ex 1787

This theorem is referenced by:  19.40  1893  moexexlem  2630  elissetv  2821  clelab  2884  elexOLD  3454  sbc5ALT  3759  dmcoss  5924  dmcossOLD  5925  suppimacnvss  8120  unblem2  9200  kmlem8  10078  isssc  17785  krull  33569  bnj1143  34979  bnj1371  35218  bnj1374  35220  bj-sbcex  36998  atex  39905  rtrclex  44068  clcnvlem  44074  pm10.55  44820