Theorem exsimpl 1870

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

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

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

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

This theorem is referenced by:  19.40  1888  moexexlem  2626  elissetv  2817  clelab  2880  elexOLD  3451  sbc5ALT  3757  dmcoss  5930  dmcossOLD  5931  suppimacnvss  8123  unblem2  9203  kmlem8  10080  isssc  17787  krull  33539  bnj1143  34932  bnj1371  35171  bnj1374  35173  bj-sbcex  36945  atex  39852  rtrclex  44044  clcnvlem  44050  pm10.55  44796