Theorem exsimpl 1870

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

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

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

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

This theorem is referenced by:  19.40  1888  moexexlem  2627  elissetv  2818  clelab  2881  elexOLD  3452  sbc5ALT  3758  dmcoss  5924  dmcossOLD  5925  suppimacnvss  8116  unblem2  9196  kmlem8  10071  isssc  17778  krull  33554  bnj1143  34948  bnj1371  35187  bnj1374  35189  bj-sbcex  36961  atex  39866  rtrclex  44062  clcnvlem  44068  pm10.55  44814