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  1006  axc11n  2311  axc11nOLD  2312  axc11nOLDOLD  2313  axc11nALT  2314  weniso  6559  infssuni  8202  ordtypelem10  8377  oismo  8390  rankval3b  8634  grur1  9587  sqeqd  13835  hausflimi  21689  minveclem4  23106  ovolunnul  23170  vitali  23283  itg2mono  23421  pilem3  24106  frgrncvvdeqlemB  27029  minvecolem4  27576  contrd  33498