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

Theorem exsimpl 1868
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 482 . 2 ((𝜑𝜓) → 𝜑)
21eximi 1835 1 (∃𝑥(𝜑𝜓) → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-ex 1780
This theorem is referenced by:  19.40  1886  moexexlem  2626  elissetv  2822  clelab  2887  elexOLD  3502  sbc5ALT  3817  r19.2zb  4496  dmcoss  5985  suppimacnvss  8198  unblem2  9329  kmlem8  10198  isssc  17864  krull  33507  bnj1143  34804  bnj1371  35043  bnj1374  35045  atex  39408  rtrclex  43630  clcnvlem  43636  pm10.55  44388
  Copyright terms: Public domain W3C validator