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

Theorem exsimpl 1870
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 1836 1 (∃𝑥(𝜑𝜓) → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781
This theorem is referenced by:  19.40  1888  moexexlem  2621  elissetv  2813  clelab  2878  elex  3492  sbc5ALT  3806  r19.2zb  4495  dmcoss  5970  suppimacnvss  8163  unblem2  9302  kmlem8  10158  isssc  17774  krull  33033  bnj1143  34264  bnj1371  34503  bnj1374  34505  atex  38740  rtrclex  42830  clcnvlem  42836  pm10.55  43590
  Copyright terms: Public domain W3C validator