Theorem exsimpl 1869

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

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

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

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

This theorem is referenced by:  19.40  1887  moexexlem  2626  elissetv  2817  clelab  2880  elexOLD  3462  sbc5ALT  3769  dmcoss  5924  dmcossOLD  5925  suppimacnvss  8115  unblem2  9193  kmlem8  10068  isssc  17744  krull  33560  bnj1143  34946  bnj1371  35185  bnj1374  35187  atex  39666  rtrclex  43858  clcnvlem  43864  pm10.55  44610