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

Theorem exsimpl 1866
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 1832 1 (∃𝑥(𝜑𝜓) → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777
This theorem is referenced by:  19.40  1884  moexexlem  2624  elissetv  2820  clelab  2885  elexOLD  3500  sbc5ALT  3820  r19.2zb  4502  dmcoss  5988  suppimacnvss  8197  unblem2  9327  kmlem8  10196  isssc  17868  krull  33487  bnj1143  34783  bnj1371  35022  bnj1374  35024  atex  39389  rtrclex  43607  clcnvlem  43613  pm10.55  44365
  Copyright terms: Public domain W3C validator