Axiomatic Schema Substitution With the following axiomatic schema (A1 - A3)
$(A1)(B \rightarrow (C \rightarrow B))$
$(A2)((B \rightarrow (C \rightarrow D)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow D)))$
$(A3)(((\lnot C) \rightarrow (\lnot B)) \rightarrow (((\lnot C) \rightarrow B) \rightarrow C))
$
I'm trying to prove that $\vdash(\lnot B \rightarrow B) \rightarrow B$
I've tried doing the following, using instances of the above:

*

*(A2) - $(((\lnot B) \rightarrow (B \rightarrow ((\lnot B))) \rightarrow (((\lnot B) \rightarrow B) \rightarrow ((\lnot B) \rightarrow (\lnot B))))$


*(A1) - $((\lnot B) \rightarrow (B \rightarrow (\lnot B)))$


*(2,3 MP) - $(((\lnot B) \rightarrow B) \rightarrow ((\lnot B) \rightarrow (\lnot B)))$


*(A3) - $(((\lnot B) \rightarrow (\lnot B)) \rightarrow (((\lnot B) \rightarrow B)) \rightarrow B))$
First off, I know this is quite simple stuff but I can't for the life of me find a way to find an antecedent to 4. using the above schema. So I'm wondering if there's something that's obviously incorrect about the process that I'm using? Is my substitution of a $B$ wf with a $(\lnot B)$ wf okay? I'm using Mendelson's book btw
 A: Let $D=B$ in $(A2)$
\begin{eqnarray*}
((B \rightarrow (C \rightarrow B)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow B)))
\end{eqnarray*}
The first clause is true ... its $(A1)$ ... so by modus ponens
\begin{eqnarray*}
 ((B \rightarrow C) \rightarrow (B \rightarrow B))
\end{eqnarray*}
Now sub $ C \rightarrow B$ for $C$
\begin{eqnarray*}
 ((B \rightarrow (C \rightarrow B)) \rightarrow (B \rightarrow B))
\end{eqnarray*}
Again the first clause is true ... its $(A1)$ ... so by modus ponens
\begin{eqnarray*}
(B \rightarrow B)
\end{eqnarray*}
Now sub $ \lnot B $ for $B$ ... so
\begin{eqnarray*}
(\lnot B \rightarrow \lnot B)
\end{eqnarray*}
So ... your fourth line & MP will give you the required result.
A: Another approach, you can establish
$$X \to Y \vdash (R \to X) \to (R \to Y)$$
Using only A1 and A2.  Then use that schema to establish
$$\lnot B \to B \vdash (\lnot B \to \lnot B) \to (\lnot B \to B)$$
Then with A3 as $$(\lnot B \to \lnot B) \to (\lnot B \to B) \vdash B$$
And just stitch things together.
