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

Theorem exsimpl 1582
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 1566 1  |-  ( E. x ( ph  /\  ps )  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531
This theorem is referenced by:  19.40  1599  euex  2179  moexex  2225  elex  2809  sbc5  3028  r19.2zb  3557  dmcoss  4960  unblem2  7126  kmlem8  7799  pm10.55  27667  bnj1143  29138  bnj1371  29375  bnj1374  29377  atex  30217
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator