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  3460  sbc5ALT  3773  r19.2zb  4449  dmcoss  5920  dmcossOLD  5921  suppimacnvss  8113  unblem2  9198  kmlem8  10071  isssc  17745  krull  33429  bnj1143  34759  bnj1371  34998  bnj1374  35000  atex  39388  rtrclex  43593  clcnvlem  43599  pm10.55  44345