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

Theorem pm2.18d 106
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 105 . 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  107  pm2.61d  153  pm2.18da  432  oplem1  932  ax10  2026  ax10lem4OLD  2031  weniso  6077  infssuni  7399  ordtypelem10  7498  oismo  7511  rankval3b  7754  grur1  8697  sqeqd  11973  bwth  17475  hausflimi  18014  minveclem4  19335  ovolunnul  19398  vitali  19507  itg2mono  19647  pilem3  20371  minvecolem4  22384  frgrancvvdeqlemB  28489  ax10lem4NEW7  29533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator