Theorem exsimpl 1864

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

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

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

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

This theorem is referenced by:  19.40  1882  moexexlem  2617  elissetv  2809  clelab  2874  elex  3488  sbc5ALT  3803  r19.2zb  4491  dmcoss  5968  suppimacnvss  8171  unblem2  9314  kmlem8  10174  isssc  17796  krull  33181  bnj1143  34411  bnj1371  34650  bnj1374  34652  atex  38868  rtrclex  43019  clcnvlem  43025  pm10.55  43778