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  1921  moexexlem  2654  elissetv  2845  clelab  2908  sbc5ALT  3771  mosubott  5491  dmcoss  5969  dmcossOLD  5970  suppimacnvss  8228  unblem2  9323  kmlem8  10275  isssc  18045  krull  34107  bnj1143  35531  bnj1371  35770  bnj1374  35772  rmo6  35821  elpssex  36672  bj-sbcex  37765  atex  40729  rtrclex  44878  clcnvlem  44884  pm10.55  45614