Prove $\lnot \lnot B$ Prove: $\lnot \lnot B$ from $\lnot \lnot A \implies \lnot \lnot B, \lnot(A \implies B) $
I cant use excluded middle: $B \lor \lnot B$
So I choose $\lnot B$ as hypothesis and will try to get $B$ which will prove $\lnot \lnot B$
$1. \lnot B$ hypothesis
$2. \lnot \lnot A \implies \lnot \lnot B$ hypothesis
$3. \lnot(A \implies B)$ hypothesis
Any idea what to do next? I have tried something like this:
$4. \lnot(A \implies B) \implies ((A \implies B) \implies B)$ axiom
$5. (A \implies B) \implies B$ MP(4, 3)
Now to get B I need $A \implies B$ which is imposible to get in this proof so this is clearly not the way to go.

I'll try to prove it in intuitionistic logic (that is, I'll try that without excluded middle.)
Lemma. It is a theorem of intuitionistic logic:
$$\lnot p\lor q\to (p\to q)$$
Proof of this lemms is not difficult: if $\lnot p$ holds, then $p\to q$ since $p\to \bot$ and $\bot \to q$ and if $q$ holds then $p\to q$ since $p,q\vdash q$ and deduction theorem.
In addition, you can check that these theorems are hold in intuitionistic logic:
(a) $\lnot\lnot\lnot p\to\lnot p$ (so $\lnot p\leftrightarrow \lnot\lnot\lnot p$)
(b) $(p\to q)\to (\lnot q\to\lnot p)$
so $\lnot \lnot A\to\lnot\lnot B$ is equivalent to $\lnot B\to\lnot A$. So we just check that
$$\lnot B\to\lnot A,\lnot(A\to B),\lnot B\vdash \bot.$$
But since $\lnot B\to\lnot A$ and $\lnot B$ implies $\lnot A$ and it implies $\lnot A\lor B$. But by lemma, it gives $A\to B$. We know that $A\to B$ and $\lnot(A\to B)$ are contradictory (without excluded middle!) Therefore, by deduction theorem we get
$$\lnot B\to\lnot A,\lnot(A\to B),\vdash \lnot B\to \bot$$
and we know that $p\to\bot$ and $\lnot p$ are equivalent.
