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 124
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 122 . 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  125  pm2.61d  170  pm2.18da  459  oplem1  1006  axc11n  2311  axc11nOLD  2312  axc11nOLDOLD  2313  axc11nALT  2314  weniso  6559  infssuni  8202  ordtypelem10  8377  oismo  8390  rankval3b  8634  grur1  9587  sqeqd  13835  hausflimi  21689  minveclem4  23106  ovolunnul  23170  vitali  23283  itg2mono  23421  pilem3  24106  frgrncvvdeqlemB  27029  minvecolem4  27576  contrd  33498
  Copyright terms: Public domain W3C validator