Theorem exsimpl 1831

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 475	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	eximi 1797	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)

Syntax hints:   → wi 4   ∧ wa 387  ∃wex 1742

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743

This theorem is referenced by:  19.40  1849  euexALTOLD  2642  moexexvw  2661  2moswapv  2662  moexex  2669  elisset  3426  elex  3433  sbc5  3708  r19.2zb  4325  dmcoss  5685  suppimacnvss  7645  unblem2  8568  kmlem8  9379  isssc  16951  bnj1143  31710  bnj1371  31946  bnj1374  31948  bj-elissetv  33684  atex  35987  rtrclex  39340  clcnvlem  39346  pm10.55  40117