Theorem exsimpl 1900

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  19.40  1918  moexexlem  2651  elissetv  2841  clelab  2904  sbc5ALT  3767  mosubott  5483  dmcoss  5957  dmcossOLD  5958  suppimacnvss  8195  unblem2  9290  kmlem8  10241  isssc  18002  krull  34051  bnj1143  35468  bnj1371  35707  bnj1374  35709  rmo6  35758  bj-sbcex  37644  atex  40570  rtrclex  44724  clcnvlem  44730  pm10.55  45460