Axiomatic Proof Of ¬(p→q)→p

This theorem serves in proof of completenes of axiom system.

Axiomatic proof follows.

[L1] ((¬(p→q)→((¬p→¬(p→q))→p))→((¬(p→q)→(¬p→¬(p→q)))→(¬(p→q)→p))) by substitution of [A2] with p↦¬(p→q), q↦(¬p→¬(p→q)), r↦p
[L2] (((¬p→¬(p→q))→p)→(¬(p→q)→((¬p→¬(p→q))→p))) by substitution of [A1] with p↦((¬p→¬(p→q))→p), q↦¬(p→q)
[L3] (((¬p→¬(p→q))→(¬¬p→p))→(((¬p→¬(p→q))→¬¬p)→((¬p→¬(p→q))→p))) by substitution of [A2] with p↦(¬p→¬(p→q)), q↦¬¬p, r↦p
[L4] ((¬¬p→p)→((¬p→¬(p→q))→(¬¬p→p))) by substitution of [A1] with p↦(¬¬p→p), q↦(¬p→¬(p→q))
[L5] ((¬¬p→((¬p→p)→p))→((¬¬p→(¬p→p))→(¬¬p→p))) by substitution of [A2] with p↦¬¬p, q↦(¬p→p), r↦p
[L6] (((¬p→p)→p)→(¬¬p→((¬p→p)→p))) by substitution of [A1] with p↦((¬p→p)→p), q↦¬¬p
[L7] (((¬p→p)→((p∨¬p)→p))→(((¬p→p)→(p∨¬p))→((¬p→p)→p))) by substitution of [A2] with p↦(¬p→p), q↦(p∨¬p), r↦p
[L8] ((p→p)→((¬p→p)→((p∨¬p)→p))) by substitution of [A8] with p↦p, r↦p, q↦¬p
[L9] ((p→((a→p)→p))→((p→(a→p))→(p→p))) by substitution of [A2] with p↦p, q↦(a→p), r↦p
[L10] (p→((a→p)→p)) by substitution of [A1] with p↦p, q↦(a→p)
[L11] ((p→(a→p))→(p→p)) by detachment of [L9] and [L10]
[L12] (p→(a→p)) by substitution of [A1] with p↦p, q↦a
[L13] (p→p) by detachment of [L11] and [L12]
[L14] ((¬p→p)→((p∨¬p)→p)) by detachment of [L8] and [L13]
[L15] (((¬p→p)→(p∨¬p))→((¬p→p)→p)) by detachment of [L7] and [L14]
[L16] ((p∨¬p)→((¬p→p)→(p∨¬p))) by substitution of [A1] with p↦(p∨¬p), q↦(¬p→p)
[L17] ((¬p→p)→(p∨¬p)) by detachment of [L16] and [A11]
[L18] ((¬p→p)→p) by detachment of [L15] and [L17]
[L19] (¬¬p→((¬p→p)→p)) by detachment of [L6] and [L18]
[L20] ((¬¬p→(¬p→p))→(¬¬p→p)) by detachment of [L5] and [L19]
[L21] (¬¬p→(¬p→p)) by substitution of [A10] with p↦¬p, q↦p
[L22] (¬¬p→p) by detachment of [L20] and [L21]
[L23] ((¬p→¬(p→q))→(¬¬p→p)) by detachment of [L4] and [L22]
[L24] (((¬p→¬(p→q))→¬¬p)→((¬p→¬(p→q))→p)) by detachment of [L3] and [L23]
[L25] ((¬p→(p→q))→((¬p→¬(p→q))→¬¬p)) by substitution of [A9] with p↦¬p, q↦(p→q)
[L26] ((¬p→¬(p→q))→¬¬p) by detachment of [L25] and [A10]
[L27] ((¬p→¬(p→q))→p) by detachment of [L24] and [L26]
[L28] (¬(p→q)→((¬p→¬(p→q))→p)) by detachment of [L2] and [L27]
[L29] ((¬(p→q)→(¬p→¬(p→q)))→(¬(p→q)→p)) by detachment of [L1] and [L28]
[L30] (¬(p→q)→(¬p→¬(p→q))) by substitution of [A1] with p↦¬(p→q), q↦¬p
[L31] (¬(p→q)→p) by detachment of [L29] and [L30]

Proof by Tableau method is here.