Theorem exsimpl 1868

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  19.40  1886  moexexlem  2620  elissetv  2810  clelab  2874  elexOLD  3472  sbc5ALT  3785  r19.2zb  4462  dmcoss  5941  suppimacnvss  8155  unblem2  9247  kmlem8  10118  isssc  17789  krull  33457  bnj1143  34787  bnj1371  35026  bnj1374  35028  atex  39407  rtrclex  43613  clcnvlem  43619  pm10.55  44365