There are three axiom in this axiomatic system $A_1$:
1. $\alpha \rightarrow (\beta \rightarrow \alpha)$
2. $(\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma))$
3. $(\neg \beta \rightarrow \neg \alpha) \rightarrow ((\neg \beta \rightarrow \alpha) \rightarrow \beta)$
Using Modus Ponens we can prove that $(\neg P \rightarrow P) \rightarrow P$ is a theorem of this axiomatic system:
1. $\neg P \rightarrow [(\neg P \rightarrow \neg P) \rightarrow \neg P]|A1$
2. $\{\neg P \rightarrow [(\neg P \rightarrow \neg P) \rightarrow \neg P]\} \rightarrow \{[\neg P \rightarrow (\neg P \rightarrow \neg P)] \rightarrow (\neg P \rightarrow \neg P)\}|A2$
3. $[\neg P \rightarrow (\neg P \rightarrow \neg P)] \rightarrow (\neg P \rightarrow \neg P)|1,2MP$
4. $\neg P \rightarrow (\neg P \rightarrow \neg P)|A1$
5. $\neg P \rightarrow \neg P|3,4MP$
6. $(\neg P \rightarrow \neg P) \rightarrow [(\neg P \rightarrow P) \rightarrow P]|A3$
7. $(\neg P \rightarrow P) \rightarrow P|5,6MP$
What I don't understand is why the first axiom ($A1$) is written twice (steps 1 and 4). The first step suggests these values for variables $\alpha$, $\beta$ and $\gamma$: $\alpha = \neg P, \beta = \neg P \rightarrow \neg P, \gamma = \neg P$, but the fourth one these: $\alpha = \neg P, \beta = \neg P, \gamma = \neg P$.
Axioms are only schemes in which you plug in wffs for variables, you can use one axiom as a scheme multiple times in a proof, pluging in different wffs for different instances of axiom.
Any axiomatic system is composed out of two types of wffs: axiomatic and wffs derived from axiomic wffs using rules of inference (since axioms are by default logical truths, wffs created from must be logical truths too, for only logical truths are allowed to be in axiomatic proof, and anything that is derived from any wff using rules of inference is logical truth, because rules of inference are truth perserving).
Since axioms are logical truths, you can use their instances more than once in a proof with different wffs, because any of those wffs created from axioms is logical truth, even if you use different values in different instances of axiom.
Sometimes you need more than one instance of axiom to prove a theorem in that axiomatic system (theorem being nothing more than wff in a proof that is not axiomatic and not assumption, i.e. wff that is derived from axiomatic wffs using rules of inference).