Theorem exsimpl 1872

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

Syntax hints:   → wi 4   ∧ wa 397  ∃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 398  df-ex 1783

This theorem is referenced by:  19.40  1890  moexexlem  2623  elissetv  2815  clelab  2880  elex  3493  sbc5ALT  3807  r19.2zb  4496  dmcoss  5971  suppimacnvss  8158  unblem2  9296  kmlem8  10152  isssc  17767  krull  32594  bnj1143  33801  bnj1371  34040  bnj1374  34042  atex  38277  rtrclex  42368  clcnvlem  42374  pm10.55  43128