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

Theorem exsimpl 1603
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 445 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21eximi 1586 1  |-  ( E. x ( ph  /\  ps )  ->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551
This theorem is referenced by:  19.40  1620  euex  2306  moexex  2352  elex  2966  sbc5  3187  r19.2zb  3720  dmcoss  5137  unblem2  7362  kmlem8  8039  isssc  14022  pm10.55  27543  bnj1143  29223  bnj1371  29460  bnj1374  29462  atex  30265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552
  Copyright terms: Public domain W3C validator