Theorem exsimpl 1868

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

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

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

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

This theorem is referenced by:  19.40  1886  moexexlem  2619  elissetv  2809  clelab  2873  elexOLD  3469  sbc5ALT  3782  r19.2zb  4459  dmcoss  5938  suppimacnvss  8152  unblem2  9240  kmlem8  10111  isssc  17782  krull  33450  bnj1143  34780  bnj1371  35019  bnj1374  35021  atex  39400  rtrclex  43606  clcnvlem  43612  pm10.55  44358