Usage of classical logical symbols in intuitionistic logic Using the Johansson's minimal logic which is a weaker form of intuitionistic logic, the author in here proves on page 83 that $A \implies B \land B \implies C$ implies $C$ holds whenever $C$ is a stable formula in the sense that $\neg \neg C \implies C$.
He defines the symbol
$ A \tilde{\lor} B \triangleq \neg A \implies \neg B \implies \bot$
and proves $A \tilde{\lor} B \implies (A \implies B) \implies (B \implies C) \implies C$.
How is it done?
Is it derived from $A \implies C \land B \implies C \land A \lor B \vdash C$?
 A: 1) $A \overline \lor B$ --- premise [1]
2) $A \to C$ --- premise [2]
3) $\lnot C$ --- assumed [a]
4) $A$ --- assumed [b]
5) $C$ --- $\to$-elim
6) $\bot$ --- from 3) and 5)
7) $\lnot A$ --- from 4) and 6), discharging [b]
8) $\lnot A \to (\lnot B \to \bot)$ --- from [1] by def
9) $\lnot B \to \bot$ --- from 7) and 8) by $\to$-elim
10) $B \to C$ --- premise [3]
11) $B$ --- assumed [c]
12) $C$ --- from 10) and 11) by $\to$-elim
13) $\bot$ --- from 3) and 12)
14) $\lnot B$ --- from 11) and 13) discharging [c]
15) $\bot$ --- from 9) and 14) by $\to$-elim
16) $\lnot \lnot C$ --- from 3) and 15), discharging [a]
17) $C$ --- from 16) and $\lnot \lnot C \to C$ : $C$ is stable

$(A \overline \lor B) \to ((A \to C) \to ((B \to C) \to C))$ --- from 1), 2), 10) and 17) bt $\to$-intros.

A: Here's a sketch of a natural deduction proof (both for the result as you have stated it and as it is given in the source that you cite): we are given assumptions:
$$
\begin{array}{lll}
(1) & \lnot A \implies \lnot B \implies \bot &\mbox{(i.e., $A\mathrel{\overline{\lor}} B$)}\\
(2) & A \implies B & \mbox{(or $A \implies C$. See comment above.)}\\
(3) & B \implies C\\
(4) & \lnot\lnot C \implies C & \mbox{(i.e., stability of $C$)}
\end{array}
$$
and we want to derive $C$. Assume $\lnot C$, i.e., assume $C \implies \bot $, then from $(3)$ we get $\lnot B$ and from $(2)$ we get $\lnot A$, so that $(1)$ gives us $\bot$. Discharging our assumption $\lnot C$, gives us that $(1)$, $(2)$ and $(3)$ imply $\lnot C \implies \bot$, i.e., $\lnot\lnot C$. But then using $(4)$, we get $C$, which is what we wanted.
