Formal proof of $(A\lor B)∨C \leftrightarrow A\lor(B\lor C)$ $A\lor B$ by definition $\neg A\implies B$
Deduction rules:


*

*$A\implies (B\implies A)$

*$(A\implies (B\implies C))\implies ((A\implies B)\implies(A\implies C))$

*$(\neg B\implies \neg A)\implies(A\implies B)$


These are axiom schemas
How to prove $(A\lor B)∨C \iff A\lor(B\lor C)$
where we need to prove $(A\lor B)∨C \implies A\lor(B\lor C)$ and $A\lor(B\lor C) \implies (A\lor B)∨C$
This is not a homework problem.
 A: As per my answer to your previous post , I'll assume that we have available the Deduction Th, that is provable (together with $\vdash A ⇒ A$) from A1) and A2) only.

For : $[¬A⇒(¬B⇒C)] \Leftrightarrow [¬(¬A⇒B)⇒C]$, we need some preliminary Lemma :

Lemma 1 : $A ⇒ B, B ⇒ C \vdash A ⇒ C$ --- Syllogism "derived rule" : easily provable with DT
Lemma 2 : $¬¬A ⇒ A$ --- Double Negation :

a) $¬¬A ⇒ (¬¬¬¬A ⇒ ¬¬A)$ --- axiom A1)
b) $(¬¬¬¬A ⇒ ¬¬A) ⇒ (¬A ⇒ ¬¬¬A)$ --- axiom A3)
c)  $¬¬A ⇒ (¬A ⇒ ¬¬¬A)$ --- from a) and b) by Lemma 1
d) $(¬A ⇒ ¬¬¬A) ⇒ (¬¬A ⇒ A)$ --- axiom A3)
e) $¬¬A ⇒ (¬¬A ⇒ A)$ --- from c) and d) by Lemma 1
f) $(¬¬A ⇒ (¬¬A ⇒ A)) ⇒ [(¬¬A ⇒ ¬¬A) ⇒ (¬¬A ⇒ A)]$ --- axiom A2)
g) $¬¬A ⇒ A$ --- from e), f) and $\vdash ¬A ⇒ ¬A$, by MP twice.

Lemma 3 : $A ⇒ ¬¬A$ --- Double Negation :

a) $¬¬¬A ⇒ ¬A$ --- Lemma 2
b) $(¬¬¬A ⇒ ¬A) ⇒ (A ⇒ ¬¬A)$ --- axiom A3)
c) $A ⇒ ¬¬A$ --- from a) and b) by MP.

Lemma 4 : $(¬B ⇒ A) ⇒ (¬A ⇒ B)$ --- provable from axiom A3), with Lemma 2 and Lemma 1.
Lemma 5 : $(A ⇒ B) ⇒ (¬¬A ⇒ ¬¬B)$ --- provable from Lemma 2, Lemma 3 and Lemma 1.
Lemma 6 : $(A ⇒ B) ⇒ (¬B ⇒ ¬A)$ --- provable from Lemma 5, axiom A3) and Lemma 1.
Lemma 7 : $¬A⇒(¬B⇒¬(¬A⇒B))$ :

a) $¬A ⇒ ((¬A⇒B) ⇒ B)$ --- from $¬A, ¬A ⇒ B \vdash B$ and DT
b) $((¬A⇒B) ⇒ B) ⇒ (¬B ⇒ ¬(¬A⇒B))$ --- Lemma 6
c) $¬A ⇒ (¬B ⇒ ¬(¬A⇒B))$ --- from a) and b) by Lemma 1.

Now for the main proof :
1) $¬(¬A⇒B)⇒C$ --- premise
2) $¬A$ --- assumed [a]
3) $¬B$ --- assumed [b]
4) $¬(¬A⇒B)$ --- from 2), 3) and Lemma 7, by Modus Ponens twice
5) $C$ --- from 4) and 1) by MP
6) $¬B⇒C$ --- from 3) and 5) by Deduction Th, discharging assumption [b]
7) $¬A⇒(¬B⇒C)$ --- from 2) and 6) by Deduction Th, discharging assumption [a]

8) $[¬(¬A⇒B)⇒C] ⇒ [¬A⇒(¬B⇒C)]$ --- from 1) and 7), discharging the premise 1)


9) $¬A⇒(¬B⇒C)$ --- premise
10) $¬A$ --- assumed [c]
11) $¬B ⇒ C$ --- from 9) and 10) by MP
12) $¬C ⇒ B$ --- from 11) and Lemma 4 by MP
13) $¬C$ --- assumed [d]
14) $B$ --- from 13) and 12) by MP
15) $¬A ⇒ B$ --- from 10) and 14) by DT, discharging assumption [c]
16) $¬C ⇒ (¬A ⇒ B)$ --- from 13) and 15) by DT, discharging assumption [d]
17) $¬(¬A ⇒ B) ⇒ C$ --- from 16) and Lemma 4 by MP

18) $[¬A⇒(¬B⇒C)] ⇒ [¬(¬A ⇒ B) ⇒ C]$ --- from 9) and 17) by DT, discharging the premise 9).




16) The bi-conditional follows from 8) and 18).


