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

Step	Hyp	Ref	Expression
1		pm2.18d.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜓))
2		pm2.18 115	. 2 ⊢ ((¬ 𝜓 → 𝜓) → 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜓)

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