MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.18d 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
Assertion
Ref Expression
pm2.18d

Proof of Theorem pm2.18d
StepHypRef Expression
1 pm2.18d.1 . 2
2 pm2.18 110 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  notnot2  112  pm2.61d  158  pm2.18da  443  oplem1  964  axc11n  2049  axc11nOLD  2050  weniso  6250  infssuni  7831  ordtypelem10  7973  oismo  7986  rankval3b  8265  grur1  9219  sqeqd  12999  bwthOLD  19911  hausflimi  20481  minveclem4  21847  ovolunnul  21911  vitali  22022  itg2mono  22160  pilem3  22848  frgrancvvdeqlemB  25038  minvecolem4  25796  contrd  30497  bj-axc11nv  34316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator