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  1883  weniso  5854  ordtypelem10  7244  oismo  7257  rankval3b  7500  fpwwe2lem13  8266  grur1  8444  sqeqd  11653  hausflimi  17677  minveclem4  18798  ovolunnul  18861  vitali  18970  itg2mono  19110  pilem3  19831  bpos  20534  minvecolem4  21461  isunscov  25085  bwt2  25603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator