MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.18d Structured version   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 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  notnot2  106  pm2.61d  152  pm2.18da  431  oplem1  931  ax10  2025  ax10lem4OLD  2030  weniso  6067  infssuni  7389  ordtypelem10  7488  oismo  7501  rankval3b  7744  grur1  8687  sqeqd  11963  bwth  17465  hausflimi  18004  minveclem4  19325  ovolunnul  19388  vitali  19497  itg2mono  19637  pilem3  20361  minvecolem4  22374  frgrancvvdeqlemB  28364  ax10lem4NEW7  29408
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator