MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exsimpl Structured version   Visualization version   GIF version

Theorem exsimpl 1871
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
StepHypRef Expression
1 simpl 483 . 2 ((𝜑𝜓) → 𝜑)
21eximi 1837 1 (∃𝑥(𝜑𝜓) → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-ex 1782
This theorem is referenced by:  19.40  1889  moexexlem  2622  elissetv  2814  clelab  2879  elex  3492  sbc5ALT  3806  r19.2zb  4495  dmcoss  5970  suppimacnvss  8157  unblem2  9295  kmlem8  10151  isssc  17766  krull  32589  bnj1143  33796  bnj1371  34035  bnj1374  34037  atex  38272  rtrclex  42358  clcnvlem  42364  pm10.55  43118
  Copyright terms: Public domain W3C validator