How to prove $\vdash\neg P\to (P\to Q)$? I am trying to prove,

$$\vdash\neg P\to (P\to Q)$$

where $P$ and $Q$ are arbitrary but otherwise fixed formulas.
The only axioms and rule of inference that I can use are,

$\color{crimson}{\text{Axiom 1.}}\  P\to (Q\to P)$
$\color{crimson}{\text{Axiom 2.}}\  (S\to (P\to Q))\to((S\to P)\to (S\to Q))$
$\color{crimson}{\text{Axiom 3.}}\  (\neg Q\to\neg P)\to(P\to Q)$
$\color{crimson}{\text{Rule of Inference.}}$ Modus Ponens.

I know that in Angelo Margaris's book First Order Mathematical Logic there is a proof (page 53) but as I have mentioned here, the dot notation seems very confusing and translating them to the nested parentheses notation seems very difficult to me. So, I am trying on my own to prove the result.
Can anyone help?
 A: Abbreviate $a = \lnot P$, $b = \lnot Q \to \lnot P$, and $c = P \to Q$. Then

$\color{crimson}{\text{1.}}\  a\to b \color{crimson}{\ \ \ \text{by axiom 1}}$
$\color{crimson}{\text{2.}}\  b\to c \color{crimson}{\ \ \ \text{by axiom 3}}$

and we need to deduce $a \to c$. The thing that ultimately is going to produce this is

$\color{crimson}{\text{3.}}\  (a \to (b \to c)) \to ((a \to b) \to (a \to c)) \color{crimson}{\ \ \ \text{by axiom 2}}$

Note that we're already very close: we just need to deduce $a \to (b \to c)$ from $b \to c$ and apply modus ponens twice. So

$\color{crimson}{\text{4.}}\  (b\to c) \to (a \to (b \to c)) \color{crimson}{\ \ \ \text{by axiom 1}}$
$\color{crimson}{\text{5.}}\  a \to (b \to c) \color{crimson}{\ \ \ \text{by modus ponens on 2 and 4}}$

And, as promised, we finish by applying modus ponens twice.

$\color{crimson}{\text{6.}}\  (a \to b) \to (a \to c) \color{crimson}{\ \ \ \text{by modus ponens on 3 and 5}}$
$\color{crimson}{\text{7.}}\  a \to c \color{crimson}{\ \ \ \text{by modus ponens on 1 and 6}}$

A: 1) $\lnot P \rightarrow (\lnot Q\rightarrow \lnot P) $ Axiom 1
2) $(\lnot Q \rightarrow \lnot P)\rightarrow (P\rightarrow Q) $ Axiom 3.
3) $[(\lnot Q \rightarrow \lnot P)\rightarrow (P\rightarrow Q)] \rightarrow \{[\lnot P \rightarrow (\lnot P\rightarrow \lnot Q)]\rightarrow [\lnot P \rightarrow(P\rightarrow Q)]\}$ Axiom 2.
4) $[\lnot P \rightarrow (\lnot P\rightarrow \lnot Q)]\rightarrow [\lnot P \rightarrow(P\rightarrow Q)]$ Modus ponens.  2 and 3 combined.
5) $\lnot P \rightarrow(P\rightarrow Q)$ Modus ponens 1 and 4 combined.
====
I originally mistated modus ponens.  Which is $A; (A \rightarrow B); \implies B$ whereas what I used was $(A \rightarrow B);(B\rightarrow C)\implies (A \rightarrow C)$ which is similar but different.
We can prove that I think:
$B \rightarrow C$ given
so by axiom 2 $(A \rightarrow B)\rightarrow (A \rightarrow C)$
$(A \rightarrow B)$ given
So $A \rightarrow C$: modus ponens.
===
As long as we are proving things I might as well prove modus nolens.
$A \rightarrow B; \lnot B$.
The $(A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)$ Axiom 3
So $\lnot B \rightarrow \lnot A$ modus ponens.
So $\lnot A$.  Modus ponens.  Hence modus nolens is valid.  Hey, this proving stuff is neat!
But I am assuming it is given $\lnot \lnot P = P$.  Is that a given?  If not we must prove it before anything.  
What are we given as basic tautologies?  Do we know $P\rightarrow P$, $P \lor \lnot P$ etc?
A: First off, let's recast those schema as well-formed formulas.  This makes substitutions mechanical and less error-prone.  Or more easily corrected when errors occur.
Axiom 1 (P$\to$(Q$\to$P))
Axiom 2 ((S$\to$(P$\to$Q))$\to$((S$\to$P)$\to$(S$\to$Q)))
Axiom 3 (($\neg$Q$\to$$\neg$P)$\to$(P$\to$Q))
We want to get to ($\neg$P$\to$(P$\to$Q)).  If we look at Axiom 3, it's consequent matches the consequent of the target formula.  So, how do we get rid of ($\neg$Q$\to$$\lnot$P) and put $\lnot$P in front of (P$\to$Q)?  Or can we do one of those two?
Well, were it the case that (P$\to$Q) was a theorem, then Axiom 1 would allow us to put any formula, such as $\neg$P, in front of (P$\to$Q).  Axiom 1 can also get used to infer any consequent of some formula $\omega$ if the antecedent of $\omega$ can get derived from Axiom 1 by substitution.  Axiom 2 "tells" us that if we have some S in front of a conditional $\chi$, we can transfer S to the front of the antecedent of $\chi$ and the front of the consequent of $\chi$.  I use $\alpha$/$\beta$ to indicate that $\alpha$ gets substituted with $\beta$.  When I write $\alpha$ * $\beta$, both $\alpha$ and $\beta$ indicate equiform formulas.  Thus, putting that all together...
:Axiom 1 P/(($\neg$Q$\to$$\neg$P)$\to$(P$\to$Q)), Q/$\neg$P * 1
1 ((($\neg$Q$\to$$\neg$P)$\to$(P$\to$Q))$\to$($\neg$P$\to$(($\neg$Q$\to$$\neg$P)$\to$(P$\to$Q))))
:1 * (Axiom 3$\to$2)
2 ($\neg$P$\to$(($\neg$Q$\to$$\neg$P)$\to$(P$\to$Q)))
:Axiom 2 S/$\neg$P, P/($\neg$Q$\to$$\neg$P), Q/(P$\to$Q) * 3
3 (($\neg$P$\to$(($\neg$Q$\to$$\neg$P)$\to$(P$\to$Q)))$\to$(($\neg$P$\to$($\neg$Q$\to$$\neg$P))$\to$($\neg$P$\to$(P$\to$Q))))
:3 * (2$\to$4)
4 (($\neg$P$\to$($\neg$Q$\to$$\neg$P))$\to$($\neg$P$\to$(P$\to$Q)))
:Axiom 1 P/$\neg$P, Q/$\neg$Q * 5
5 ($\neg$P$\to$($\neg$Q$\to$$\neg$P))
:4 * (5$\to$6)
6 ($\neg$P$\to$(P$\to$Q))
The above is a bit of false history if read as indicating how I found this proof, but perhaps it also offers a bit more metalogical insight.
A: Hint: Use Axiom 1 in the form $\neg P \to (\neg Q \to \neg P)$ and Axiom 3.
