Deducing $((\neg a \to \neg b) \to ((\neg a \to b) \to b)))$ from axioms I have seen many questions here, using a different set of axioms than mine.

Here is mine :

$$1) (a \to (b \to a))$$
$$2) ((a \to (b \to c)) \to ((a \to b) \to (a \to c)))$$
$$3) ((\neg b \to \neg a) \to (a \to b))$$

Is it possible to deduce the following from these: $((a \to b) \to ((\neg a \to b) \to b))$.

I couldn't find a proof myself or online.

Thank you very much!!!
Undoubtedly a shorter proof exists, but here's a Prover9 proof:

% -------- Comments from original proof --------

% Proof 1 at 208.84 (+ 24.69) seconds.

% Length of proof is 53.

% Level of proof is 20.

% Maximum clause weight is 24.

% Given clauses 9783.

1 P((x -> y) -> ((-x -> y) -> y)) # label(non_clause) # label(goal).  [goal].

2 -P(x -> y) | -P(x) | P(y).  [assumption].

3 P(x -> (y -> x)).  [assumption].

4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))).  [assumption].

5 P((-x -> -y) -> (y -> x)).  [assumption].

6 -P((c1 -> c2) -> ((-c1 -> c2) -> c2)).  [deny(1)].

7 P(x -> (y -> (z -> y))).  [hyper(2,a,3,a,b,3,a)].

8 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))).  [hyper(2,a,4,a,b,4,a)].

9 P(x -> ((y -> (z -> u)) -> ((y -> z) -> (y -> u)))).  [hyper(2,a,3,a,b,4,a)].

10 P((x -> y) -> (x -> x)).  [hyper(2,a,4,a,b,3,a)].

11 P(((-x -> -y) -> y) -> ((-x -> -y) -> x)).  [hyper(2,a,4,a,b,5,a)].

12 P(x -> ((-y -> -z) -> (z -> y))).  [hyper(2,a,3,a,b,5,a)].

14 P(x -> (y -> (z -> (u -> z)))).  [hyper(2,a,3,a,b,7,a)].

17 P(x -> x).  [hyper(2,a,10,a,b,7,a)].

18 P(((x -> y) -> x) -> ((x -> y) -> y)).  [hyper(2,a,4,a,b,17,a)].

26 P((x -> ((y -> x) -> z)) -> (x -> z)).  [hyper(2,a,8,a,b,7,a)].

44 P((x -> ((y -> (z -> y)) -> u)) -> (x -> u)).  [hyper(2,a,8,a,b,14,a)].

48 P(((x -> (y -> z)) -> (((x -> y) -> (x -> z)) -> u)) -> ((x -> (y -> z)) -> u)).  [hyper(2,a,8,a,b,9,a)].

71 P((x -> (-y -> -z)) -> (x -> (z -> y))).  [hyper(2,a,4,a,b,12,a)].

159 P(-x -> (x -> y)).  [hyper(2,a,26,a,b,12,a)].

160 P((x -> y) -> ((z -> x) -> (z -> y))).  [hyper(2,a,26,a,b,9,a)].

166 P(x -> (-y -> (y -> z))).  [hyper(2,a,3,a,b,159,a)].

197 P(((-x -> (x -> y)) -> z) -> z).  [hyper(2,a,18,a,b,166,a)].

815 P(((x -> y) -> z) -> (y -> z)).  [hyper(2,a,44,a,b,160,a)].

835 P(x -> (((y -> z) -> u) -> (z -> u))).  [hyper(2,a,3,a,b,815,a)].

841 P(x -> ((x -> y) -> y)).  [hyper(2,a,815,a,b,18,a)].

842 P(x -> ((-y -> -x) -> y)).  [hyper(2,a,815,a,b,11,a)].

915 P(((x -> ((x -> y) -> y)) -> z) -> z).  [hyper(2,a,841,a,b,841,a)].

918 P((x -> y) -> (x -> ((y -> z) -> z))).  [hyper(2,a,160,a,b,841,a)].

1299 P((x -> (-y -> -x)) -> (x -> y)).  [hyper(2,a,4,a,b,842,a)].

3180 P((x -> (y -> z)) -> (y -> (x -> z))).  [hyper(2,a,48,a,b,835,a)].

3224 P(x -> ((((x -> y) -> y) -> z) -> z)).  [hyper(2,a,915,a,b,918,a)].

4594 P(--x -> x).  [hyper(2,a,197,a,b,1299,a)].

4644 P(--x -> ((x -> y) -> y)).  [hyper(2,a,918,a,b,4594,a)].

4672 P(x -> --x).  [hyper(2,a,5,a,b,4594,a)].

4728 P((x -> y) -> (x -> --y)).  [hyper(2,a,160,a,b,4672,a)].

7577 P((-x -> y) -> (-y -> x)).  [hyper(2,a,71,a,b,4728,a)].

19603 P(x -> ((x -> y) -> --y)).  [hyper(2,a,3180,a,b,4728,a)].

19609 P((x -> y) -> (--x -> y)).  [hyper(2,a,3180,a,b,4644,a)].

19633 P((x -> y) -> ((y -> z) -> (x -> z))).  [hyper(2,a,3180,a,b,160,a)].

20528 P(--x -> ((x -> y) -> --y)).  [hyper(2,a,19609,a,b,19603,a)].

23007 P((((x -> y) -> y) -> z) -> (x -> z)).  [hyper(2,a,3180,a,b,3224,a)].

25963 P(((--x -> y) -> z) -> ((x -> y) -> z)).  [hyper(2,a,19633,a,b,19609,a)].

26004 P(((-x -> y) -> z) -> ((-y -> x) -> z)).  [hyper(2,a,19633,a,b,7577,a)].

26321 P((x -> y) -> (--x -> --y)).  [hyper(2,a,3180,a,b,20528,a)].

27746 P((x -> y) -> (-y -> -x)).  [hyper(2,a,71,a,b,26321,a)].

27754 P(x -> (-y -> -(x -> y))).  [hyper(2,a,23007,a,b,27746,a)].

28030 P(-x -> (y -> -(y -> x))).  [hyper(2,a,3180,a,b,27754,a)].

28135 P((-x -> y) -> (-x -> -(y -> x))).  [hyper(2,a,4,a,b,28030,a)].

29738 P((-x -> y) -> ((y -> x) -> x)).  [hyper(2,a,71,a,b,28135,a)].

34389 P((-x -> y) -> ((x -> y) -> y)).  [hyper(2,a,26004,a,b,29738,a)].

34398 P((x -> y) -> ((-x -> y) -> y)).  [hyper(2,a,25963,a,b,34389,a)].

34399 $F.  [resolve(34398,a,6,a)].

Edit: Here's a shorter proof via OTTER.  OTTER has found shorter proofs also, but they took more time for OTTER to find.

----> UNIT CONFLICT at   2.23 sec ----> 8034 [binary,8033.1,2.1] $F.

Length of proof is 36.  Level of proof is 18.

---------------- PROOF ----------------

1 [] -P(C(x,y))| -P(x)|P(y).

2 [] -P(C(C(a,b),C(C(N(a),b),b))).

3 [] P(C(x,C(y,x))).

4 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).

5 [] P(C(C(N(x),N(y)),C(y,x))).

6 [hyper,1,3,3] P(C(x,C(y,C(z,y)))).

7 [hyper,1,3,4] P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))).

8 [hyper,1,4,3] P(C(C(x,y),C(x,x))).

9 [hyper,1,3,5] P(C(x,C(C(N(y),N(z)),C(z,y)))).

10 [hyper,1,4,6] P(C(C(x,y),C(x,C(z,y)))).

15 [hyper,1,8,3] P(C(x,x)).

16 [hyper,1,4,15] P(C(C(C(x,y),x),C(C(x,y),y))).

21 [hyper,1,3,10] P(C(x,C(C(y,z),C(y,C(u,z))))).

23 [hyper,1,10,4] P(C(C(x,C(y,z)),C(u,C(C(x,y),C(x,z))))).

35 [hyper,1,3,16] P(C(x,C(C(C(y,z),y),C(C(y,z),z)))).

39 [hyper,1,16,6] P(C(C(C(x,C(y,x)),z),z)).

58 [hyper,1,4,21] P(C(C(x,C(y,z)),C(x,C(y,C(u,z))))).

74 [hyper,1,3,39] P(C(x,C(C(C(y,C(z,y)),u),u))).

136 [hyper,1,4,74] P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))).

191 [hyper,1,136,5] P(C(C(N(x),N(C(y,C(z,y)))),x)).

192 [hyper,1,136,4] P(C(C(x,C(C(y,x),z)),C(x,z))).

199 [hyper,1,192,35] P(C(x,C(C(x,y),y))).

200 [hyper,1,192,9] P(C(N(x),C(x,y))).

201 [hyper,1,192,7] P(C(C(x,y),C(C(z,x),C(z,y)))).

215 [hyper,1,4,200] P(C(C(N(x),x),C(N(x),y))).

216 [hyper,1,3,200] P(C(x,C(N(y),C(y,z)))).

230 [hyper,1,3,215] P(C(x,C(C(N(y),y),C(N(y),z)))).

258 [hyper,1,3,199] P(C(x,C(y,C(C(y,z),z)))).

271 [hyper,1,23,201] P(C(x,C(C(C(y,z),C(u,y)),C(C(y,z),C(u,z))))).

274 [hyper,1,4,201] P(C(C(C(x,y),C(z,x)),C(C(x,y),C(z,y)))).

1921 [hyper,1,192,271] P(C(C(x,y),C(C(y,z),C(x,z)))).

2066 [hyper,1,274,258] P(C(C(C(C(x,y),y),z),C(x,z))).

2070 [hyper,1,274,230] P(C(C(C(N(x),y),z),C(C(N(x),x),z))).

2072 [hyper,1,274,216] P(C(C(C(x,y),z),C(N(x),z))).

2197 [hyper,1,2070,191] P(C(C(N(x),x),x)).

2204 [hyper,1,201,2197] P(C(C(x,C(N(y),y)),C(x,y))).

7657 [hyper,1,2204,2066] P(C(C(C(C(N(x),y),y),x),x)).

7700 [hyper,1,2072,7657] P(C(N(C(C(N(x),y),y)),x)).

7727 [hyper,1,1921,7700] P(C(C(x,y),C(N(C(C(N(x),z),z)),y))).

7831 [hyper,1,58,7727] P(C(C(x,y),C(N(C(C(N(x),z),z)),C(u,y)))).

8033 [hyper,1,2204,7831] P(C(C(x,y),C(C(N(x),y),y))).

8034 [binary,8033.1,2.1] $F.

------------ end of proof -------------
It helps to know:


Two logical expressions are equivalent iff they have the same truth table
$(a \rightarrow b) \leftrightarrow (\neg a \vee b) $ (One can proof that using the truth table)
$(a \rightarrow b) \leftrightarrow (\neg b \rightarrow \neg a) $ (One can proof that using the truth table)
$(a \vee \neg a) =1$ (Tautology)
$\neg \neg a = a$ (Double negation)
$1$ is the neutral element of the logical conjuction: $1\wedge a = a$




Here is my approach to deduce the given expression from elementary propositions:

Let $a$ and $b$ be two propositions, with 
$$a \rightarrow b$$
$$ \leftrightarrow \neg a \vee b$$ 
$$\leftrightarrow (\neg a \wedge b)\vee(\neg a \vee b)$$
$$\leftrightarrow (\neg (a \vee \neg b))\vee(\neg a \vee b)$$
$$\leftrightarrow (a \vee \neg b)\rightarrow (\neg a \vee b)$$
$$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a)$$
$$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a) \wedge 1 $$
$$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a) \wedge (b \vee \neg b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee( \neg a \wedge \neg b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg(a \vee b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg(\neg \neg a \vee b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg( \neg a \rightarrow b) $$
$$\leftrightarrow (a \vee \neg b)\rightarrow \neg( \neg a \rightarrow b) \vee b $$
$$\leftrightarrow (a \vee \neg b)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$
$$\leftrightarrow (\neg b \vee a)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$
$$\leftrightarrow (b \rightarrow a)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$
$$\leftrightarrow (\neg a \rightarrow \neg b)\rightarrow (( \neg a \rightarrow b) \rightarrow b)$$