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

Theorem pm2.18d 122
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 120 . 2 ((¬ 𝜓𝜓) → 𝜓)
31, 2syl 17 1 (𝜑𝜓)
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:  notnotr  123  pm2.61d  168  pm2.18da  457  oplem1  998  axc11n  2199  axc11nOLD  2200  axc11nOLDOLD  2201  axc11nALT  2202  weniso  6380  infssuni  8015  ordtypelem10  8190  oismo  8203  rankval3b  8447  grur1  9396  sqeqd  13611  hausflimi  21495  minveclem4  22875  minveclem4OLD  22887  ovolunnul  22951  vitali  23064  itg2mono  23202  pilem3  23899  frgrancvvdeqlemB  26304  minvecolem4  26899  minvecolem4OLD  26909  contrd  32944  frgrncvvdeqlemB  41569
  Copyright terms: Public domain W3C validator