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 125
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 123 . 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:  pm2.61d  171  pm2.18da  801  oplem1  1043  axc11n  2462  weniso  6747  infssuni  8413  ordtypelem10  8588  oismo  8601  rankval3b  8853  grur1  9844  sqeqd  14114  hausflimi  22004  minveclem4  23422  ovolunnul  23488  vitali  23601  itg2mono  23740  pilem3OLD  24428  frgrncvvdeqlem8  27488  minvecolem4  28076  contrd  34231
  Copyright terms: Public domain W3C validator