How do I prove ¬¬p → p

Stream: new members

[Lars Ericson]

This is probably dead simple but I am really going in circles. This:

lemma not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := iff.rfl

theorem negneg (p : Prop) : ¬¬p → p :=
begin
  intro h,
  rw not_iff_imp_false (¬p) at h,
  rw not_iff_imp_false p at h,
  by_cases hp : p → false,
  exfalso,
  apply hp,
  exfalso,
  exact h hp,
  end

leaves me in goal state

p : Prop,
h : (p → false) → false,
hp : ¬(p → false)
⊢ p

[Donald Sebastian Leung]

In negneg, introduce the ¬¬p hypothesis then use proof by_contradiction.

[Lars Ericson]

Thank you @Donald Sebastian Leung that's actually my first successful use of by_contra:

theorem negneg (p : Prop) : ¬¬p → p :=
begin
  intro h,
  by_contra h1,
  exact h h1,
end