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

Theorem pm2.18d 103
Description: Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
pm2.18d.1  |-  ( ph  ->  ( -.  ps  ->  ps ) )
Assertion
Ref Expression
pm2.18d  |-  ( ph  ->  ps )

Proof of Theorem pm2.18d
StepHypRef Expression
1 pm2.18d.1 . 2  |-  ( ph  ->  ( -.  ps  ->  ps ) )
2 pm2.18 102 . 2  |-  ( ( -.  ps  ->  ps )  ->  ps )
31, 2syl 15 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  notnot2  104  pm2.61d  150  pm2.18da  430  oplem1  930  ax10lem4  1894  weniso  5868  ordtypelem10  7258  oismo  7271  rankval3b  7514  fpwwe2lem13  8280  grur1  8458  sqeqd  11667  hausflimi  17691  minveclem4  18812  ovolunnul  18875  vitali  18984  itg2mono  19124  pilem3  19845  bpos  20548  minvecolem4  21475  isunscov  25177  bwt2  25695  ax10lem4NEW7  29448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator