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  2294  axc11nOLD  2295  axc11nOLDOLD  2296  axc11nALT  2297  weniso  6482  infssuni  8117  ordtypelem10  8292  oismo  8305  rankval3b  8549  grur1  9498  sqeqd  13700  hausflimi  21536  minveclem4  22928  ovolunnul  22992  vitali  23105  itg2mono  23243  pilem3  23928  frgrancvvdeqlemB  26331  minvecolem4  26926  contrd  32865  frgrncvvdeqlemB  41472
  Copyright terms: Public domain W3C validator