Theorem exsimpl 1871

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  19.40  1889  moexexlem  2628  elissetv  2819  clelab  2883  elex  3450  sbc5ALT  3745  r19.2zb  4426  dmcoss  5880  suppimacnvss  7989  unblem2  9067  kmlem8  9913  isssc  17532  krull  31643  bnj1143  32770  bnj1371  33009  bnj1374  33011  atex  37420  rtrclex  41225  clcnvlem  41231  pm10.55  41987