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

Theorem exsimpl 1579
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  |-  ( E. x ( ph  /\  ps )  ->  E. x ph )

Proof of Theorem exsimpl
StepHypRef Expression
1 simpl 443 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21eximi 1563 1  |-  ( E. x ( ph  /\  ps )  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528
This theorem is referenced by:  19.40  1596  euex  2166  moexex  2212  elex  2796  sbc5  3015  r19.2zb  3544  dmcoss  4944  unblem2  7110  kmlem8  7783  pm10.55  27564  bnj1143  28822  bnj1371  29059  bnj1374  29061  atex  29595
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator