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  5813  ordtypelem10  7237  oismo  7250  rankval3b  7493  fpwwe2lem13  8259  grur1  8437  sqeqd  11646  hausflimi  17670  minveclem4  18791  ovolunnul  18854  vitali  18963  itg2mono  19103  pilem3  19824  bpos  20527  minvecolem4  21452  isunscov  24484  bwt2  25003
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator