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

Theorem pm2.18d 111
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 110 . 2  |-  ( ( -.  ps  ->  ps )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  notnot2  112  pm2.61d  158  pm2.18da  443  oplem1  957  axc11n  2017  axc11nOLD  2018  weniso  6231  infssuni  7802  ordtypelem10  7943  oismo  7956  rankval3b  8235  grur1  9189  sqeqd  12951  bwthOLD  19672  hausflimi  20211  minveclem4  21577  ovolunnul  21641  vitali  21752  itg2mono  21890  pilem3  22577  frgrancvvdeqlemB  24703  minvecolem4  25460  bj-axc11nv  33274
  Copyright terms: Public domain W3C validator