Theorem exsimpl 1867

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

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

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

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

This theorem is referenced by:  19.40  1885  moexexlem  2629  elissetv  2825  clelab  2890  elexOLD  3510  sbc5ALT  3833  r19.2zb  4519  dmcoss  5997  suppimacnvss  8214  unblem2  9357  kmlem8  10227  isssc  17881  krull  33472  bnj1143  34766  bnj1371  35005  bnj1374  35007  atex  39363  rtrclex  43579  clcnvlem  43585  pm10.55  44338