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 117
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 115 . 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  118  pm2.61d  165  pm2.18da  452  oplem1  989  axc11n  2191  axc11nOLD  2192  axc11nALT  2193  weniso  6318  infssuni  7950  ordtypelem10  8125  oismo  8138  rankval3b  8382  grur1  9330  sqeqd  13389  hausflimi  21153  minveclem4  22533  minveclem4OLD  22545  ovolunnul  22612  vitali  22732  itg2mono  22872  pilem3  23570  pilem3OLD  23571  frgrancvvdeqlemB  25926  minvecolem4  26685  minvecolem4OLD  26695  bj-axc11nv  31535  contrd  32570  frgrncvvdeqlemB  40877
  Copyright terms: Public domain W3C validator