It may be slightly easier to work through it for the formula ¬¬¬P ⇒ ¬P. (This also a constructive tautology, and the above formula is an instance of it, taking P = ¬ϕ). So let's prove that.
Expanding the definition of ¬, we must prove (((P⇒False)⇒False)⇒False)⇒P⇒False. I.e. we are given two assumptions
f : ((P⇒False)⇒False)⇒False
x : P
and should prove False. So we can use the assumption f, provided we can find an argument of type ((P⇒False)⇒False) to call it with. And in fact that's easy: (λg. g x). The full proof term is λf.λx. f (λg. g x)
Indeed, this is a perfectly good function (so it's constructive). If we type that function into (say) a Haskell repl, the typechecker will infer an even more general type for it, but we can check that the type we wanted is an instance:
ghci> :type (\f x -> f (\g -> g x))
(\f x -> f (\g -> g x)) :: (((t2->t1)->t1)->t) -> t2 -> t
gchi> type Not a = (a -> False)
ghci> :type (\f x -> f (\g -> g x)) :: (Not (Not (Not p)))->Not p
(\f x -> f (\g -> g x)) :: (Not (Not (Not p))) -> Not p
It just follows from the axioms. They accept that a proof of ¬ p can be a proof that takes p and arrives to a contradiction. And that a contradiction is a formula and its negation. From that we can prove ¬¬¬¬p => ¬¬p.
We can assume ¬p and we have to prove a contradiction.
So we have to prove: ¬¬¬¬p, ¬p => _|_
Now, we know* that alpha => ¬¬alpha.
So from ¬p, we can get ¬¬¬p.
And from ¬(¬¬¬p) and (¬¬¬p) we arrive to _|_.
*To prove alpha => ¬¬alpha, we can assume ¬alpha and arrive at a contradiction, so we would have to rpove alpha, ¬alpha => _|_ and we are done.
This has been generalized to translate classical theorems into constructive theorems.[1] Just like this case, though, the resulting theorems are full of double negations.
¬¬¬¬ϕ ⇒ ¬¬ϕ