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

Theorem pm2.18d 115
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 114 . 2  |-  ( ( -.  ps  ->  ps )  ->  ps )
31, 2syl 17 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  116  pm2.61d  162  pm2.18da  445  oplem1  975  axc11n  2143  axc11nALT  2144  weniso  6245  infssuni  7865  ordtypelem10  8042  oismo  8055  rankval3b  8297  grur1  9245  sqeqd  13229  hausflimi  20995  minveclem4  22374  minveclem4OLD  22386  ovolunnul  22453  vitali  22571  itg2mono  22711  pilem3  23409  pilem3OLD  23410  frgrancvvdeqlemB  25766  minvecolem4  26522  minvecolem4OLD  26532  bj-axc11nv  31348  contrd  32333
  Copyright terms: Public domain W3C validator