Theorem pm2.18d 124

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 122	. 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  125  pm2.61d  170  pm2.18da  459  oplem1  1007  axc11n  2307  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  weniso  6604  infssuni  8257  ordtypelem10  8432  oismo  8445  rankval3b  8689  grur1  9642  sqeqd  13906  hausflimi  21784  minveclem4  23203  ovolunnul  23268  vitali  23382  itg2mono  23520  pilem3  24207  frgrncvvdeqlem8  27170  minvecolem4  27736  contrd  33899