Axiomatic Proof Of (¬p→p)→p

This theorem serves in proof of completenes of axiom system.

Axiomatic proof follows.

[L1] (((¬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
[L2] ((p→p)→((¬p→p)→((p∨¬p)→p))) by substitution of [A8] with p↦p, r↦p, q↦¬p
[L3] ((p→((a→p)→p))→((p→(a→p))→(p→p))) by substitution of [A2] with p↦p, q↦(a→p), r↦p
[L4] (p→((a→p)→p)) by substitution of [A1] with p↦p, q↦(a→p)
[L5] ((p→(a→p))→(p→p)) by detachment of [L3] and [L4]
[L6] (p→(a→p)) by substitution of [A1] with p↦p, q↦a
[L7] (p→p) by detachment of [L5] and [L6]
[L8] ((¬p→p)→((p∨¬p)→p)) by detachment of [L2] and [L7]
[L9] (((¬p→p)→(p∨¬p))→((¬p→p)→p)) by detachment of [L1] and [L8]
[L10] ((p∨¬p)→((¬p→p)→(p∨¬p))) by substitution of [A1] with p↦(p∨¬p), q↦(¬p→p)
[L11] ((¬p→p)→(p∨¬p)) by detachment of [L10] and [A11]
[L12] ((¬p→p)→p) by detachment of [L9] and [L11]

Proof by Tableau method is here.