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  1881  weniso  5852  ordtypelem10  7242  oismo  7255  rankval3b  7498  fpwwe2lem13  8264  grur1  8442  sqeqd  11651  hausflimi  17675  minveclem4  18796  ovolunnul  18859  vitali  18968  itg2mono  19108  pilem3  19829  bpos  20532  minvecolem4  21459  isunscov  25074  bwt2  25592
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator