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 123
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 121 . 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  124  pm2.61d  169  pm2.18da  458  oplem1  999  axc11n  2295  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  weniso  6504  infssuni  8140  ordtypelem10  8315  oismo  8328  rankval3b  8572  grur1  9521  sqeqd  13754  hausflimi  21594  minveclem4  23011  ovolunnul  23075  vitali  23188  itg2mono  23326  pilem3  24011  frgrancvvdeqlemB  26565  minvecolem4  27120  contrd  33069  frgrncvvdeqlemB  41477
  Copyright terms: Public domain W3C validator