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  964  axc11n  2035  axc11nOLD  2036  weniso  6235  infssuni  7813  ordtypelem10  7955  oismo  7968  rankval3b  8247  grur1  9201  sqeqd  12981  bwthOLD  19889  hausflimi  20459  minveclem4  21825  ovolunnul  21889  vitali  22000  itg2mono  22138  pilem3  22826  frgrancvvdeqlemB  25016  minvecolem4  25774  contrd  30473  bj-axc11nv  34199
  Copyright terms: Public domain W3C validator