A question about Implicational Propositional Calculus My question is motivated by a previous post about Implicational calculus
Having showed that Mendelson (A1) and (A2) axioms plus Peirce's law are a complete axiom set for implicational fragment of propositional calculus, where :

(A1) $\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{B})$
(A2) $(\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{D})) \rightarrow ((\mathcal{B} \rightarrow \mathcal{C}) \rightarrow (\mathcal{B} \rightarrow \mathcal{D}))$

and Peirce's law is :

$((\mathcal{A} \rightarrow \mathcal{B}) \rightarrow \mathcal{A}) \rightarrow \mathcal{A}$

I'm not able to derive (A3), where :
(A3) $(\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$.
In order to extend implicational calculus to full propositional calculus I assume that we need to introduce $\bot$, in order to define $\lnot \mathcal{A}$ as $\mathcal{A} \rightarrow \bot$.
But I'm still unable to find the solution.

I think I sorted out the outline, I still need to fill in the gaps but here something to start with:
(f = $ \bot $)
1  |- ( A -> (B->C)) -> ((A -> B)-> (A->C)))                 A2 
2  |- ( A -> (B->f)) -> ((A -> B)-> (A->f)))                 1 C := f
3  |- ( (A->f) -> (B->f) )-> (((A->f) -> B)-> ((A->f)->f)))  2 A := (A->f)
4  |- ((A -> B) -> A) -> A                                   A3 Peirce
5  |- ((A->f) -> A) -> A                                     4  B := f 
6  |- ((A->f) -> f) -> ((A->f) -> f)                         theorem (A -> A)
7  |- f -> A                                                 axiom 
8  |- ((A -> f) -> f) -> ((A -> f) -> A)                     hyp syll 6,7 
9  |- ((A -> f) -> f) -> A                                   hyp syll 8,5
10 |- ((A -> f) -> (B-> f)) -> (((A ->f) -> B)-> A )         hyp syll 3,9

And 10 is $  ( \lnot A  \to \lnot B) \to (( \lnot A  \to B) \to A ) $ 
good exercise 
