Axiomatic Proof Of (p→q)→((¬p→q)→q)

This theorem serves in proof of completenes of axiom system.

Axiomatic proof follows.

[L1] (((p→q)→(((¬p→q)→(p∨¬p))→((¬p→q)→q)))→(((p→q)→((¬p→q)→(p∨¬p)))→((p→q)→((¬p→q)→q)))) by substitution of [A2] with p↦(p→q), q↦((¬p→q)→(p∨¬p)), r↦((¬p→q)→q)
[L2] (((p→q)→(((¬p→q)→((p∨¬p)→q))→(((¬p→q)→(p∨¬p))→((¬p→q)→q))))→(((p→q)→((¬p→q)→((p∨¬p)→q)))→((p→q)→(((¬p→q)→(p∨¬p))→((¬p→q)→q))))) by substitution of [A2] with p↦(p→q), q↦((¬p→q)→((p∨¬p)→q)), r↦(((¬p→q)→(p∨¬p))→((¬p→q)→q))
[L3] ((((¬p→q)→((p∨¬p)→q))→(((¬p→q)→(p∨¬p))→((¬p→q)→q)))→((p→q)→(((¬p→q)→((p∨¬p)→q))→(((¬p→q)→(p∨¬p))→((¬p→q)→q))))) by substitution of [A1] with p↦(((¬p→q)→((p∨¬p)→q))→(((¬p→q)→(p∨¬p))→((¬p→q)→q))), q↦(p→q)
[L4] (((¬p→q)→((p∨¬p)→q))→(((¬p→q)→(p∨¬p))→((¬p→q)→q))) by substitution of [A2] with p↦(¬p→q), q↦(p∨¬p), r↦q
[L5] ((p→q)→(((¬p→q)→((p∨¬p)→q))→(((¬p→q)→(p∨¬p))→((¬p→q)→q)))) by detachment of [L3] and [L4]
[L6] (((p→q)→((¬p→q)→((p∨¬p)→q)))→((p→q)→(((¬p→q)→(p∨¬p))→((¬p→q)→q)))) by detachment of [L2] and [L5]
[L7] ((p→q)→((¬p→q)→((p∨¬p)→q))) by substitution of [A8] with p↦p, r↦q, q↦¬p
[L8] ((p→q)→(((¬p→q)→(p∨¬p))→((¬p→q)→q))) by detachment of [L6] and [L7]
[L9] (((p→q)→((¬p→q)→(p∨¬p)))→((p→q)→((¬p→q)→q))) by detachment of [L1] and [L8]
[L10] (((¬p→q)→(p∨¬p))→((p→q)→((¬p→q)→(p∨¬p)))) by substitution of [A1] with p↦((¬p→q)→(p∨¬p)), q↦(p→q)
[L11] ((p∨¬p)→((¬p→q)→(p∨¬p))) by substitution of [A1] with p↦(p∨¬p), q↦(¬p→q)
[L12] ((¬p→q)→(p∨¬p)) by detachment of [L11] and [A11]
[L13] ((p→q)→((¬p→q)→(p∨¬p))) by detachment of [L10] and [L12]
[L14] ((p→q)→((¬p→q)→q)) by detachment of [L9] and [L13]

Proof by Tableau method is here.