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

Theorem exsimpl 1831
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 475 . 2 ((𝜑𝜓) → 𝜑)
21eximi 1797 1 (∃𝑥(𝜑𝜓) → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wex 1742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743
This theorem is referenced by:  19.40  1849  euexALTOLD  2642  moexexvw  2661  2moswapv  2662  moexex  2669  elisset  3426  elex  3433  sbc5  3708  r19.2zb  4325  dmcoss  5685  suppimacnvss  7645  unblem2  8568  kmlem8  9379  isssc  16951  bnj1143  31710  bnj1371  31946  bnj1374  31948  bj-elissetv  33684  atex  35987  rtrclex  39340  clcnvlem  39346  pm10.55  40117
  Copyright terms: Public domain W3C validator