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

Theorem pm2.18d 105
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 104 . 2  |-  ( ( -.  ps  ->  ps )  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  notnot2  106  pm2.61d  152  pm2.18da  432  oplem1  935  ax10lem26  1675  weniso  5751  ordtypelem10  7175  oismo  7188  rankval3b  7431  fpwwe2lem13  8197  grur1  8375  sqeqd  11581  hausflimi  17602  minveclem4  18723  ovolunnul  18786  vitali  18895  itg2mono  19035  pilem3  19756  bpos  20459  minvecolem4  21384  isunscov  24405  bwt2  24924  ax10lem26X  28225
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator