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  458  oplem1  1027  axc11n  2342  axc11nOLD  2343  weniso  6644  infssuni  8298  ordtypelem10  8473  oismo  8486  rankval3b  8727  grur1  9680  sqeqd  13950  hausflimi  21831  minveclem4  23249  ovolunnul  23314  vitali  23427  itg2mono  23565  pilem3  24252  frgrncvvdeqlem8  27286  minvecolem4  27864  contrd  34029
  Copyright terms: Public domain W3C validator