Theorem exsimpl 1876

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1787

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788

This theorem is referenced by:  19.40  1894  moexexlem  2627  elissetv  2811  clelab  2873  elex  3416  sbc5ALT  3712  r19.2zb  4393  dmcoss  5825  suppimacnvss  7893  unblem2  8902  kmlem8  9736  isssc  17279  krull  31311  bnj1143  32437  bnj1371  32676  bnj1374  32678  bj-elissetv  34747  atex  37106  rtrclex  40842  clcnvlem  40848  pm10.55  41601