Theorem exsimpl 1869

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

Syntax hints:   → wi 4   ∧ wa 394  ∃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 206  df-an 395  df-ex 1780

This theorem is referenced by:  19.40  1887  moexexlem  2620  elissetv  2812  clelab  2877  elex  3491  sbc5ALT  3805  r19.2zb  4494  dmcoss  5969  suppimacnvss  8160  unblem2  9298  kmlem8  10154  isssc  17771  krull  32868  bnj1143  34099  bnj1371  34338  bnj1374  34340  atex  38580  rtrclex  42670  clcnvlem  42676  pm10.55  43430