Theorem exsimpl 1901

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

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

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

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

This theorem is used by:  19.40  1919  moexexlem  2652  elissetv  2842  clelab  2905  sbc5ALT  3768  mosubott  5484  dmcoss  5957  dmcossOLD  5958  suppimacnvss  8183  unblem2  9278  kmlem8  10229  isssc  17988  krull  33996  bnj1143  35413  bnj1371  35652  bnj1374  35654  bj-sbcex  37530  atex  40443  rtrclex  44602  clcnvlem  44608  pm10.55  45338