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

This theorem serves in proof of completenes of axiom system.

Axiomatic proof follows.

[L1] ((¬(p→q)→((q→¬(p→q))→¬q))→((¬(p→q)→(q→¬(p→q)))→(¬(p→q)→¬q))) by substitution of [A2] with p↦¬(p→q), q↦(q→¬(p→q)), r↦¬q
[L2] (((q→¬(p→q))→¬q)→(¬(p→q)→((q→¬(p→q))→¬q))) by substitution of [A1] with p↦((q→¬(p→q))→¬q), q↦¬(p→q)
[L3] ((q→(p→q))→((q→¬(p→q))→¬q)) by substitution of [A9] with p↦q, q↦(p→q)
[L4] (q→(p→q)) by substitution of [A1] with p↦q, q↦p
[L5] ((q→¬(p→q))→¬q) by detachment of [L3] and [L4]
[L6] (¬(p→q)→((q→¬(p→q))→¬q)) by detachment of [L2] and [L5]
[L7] ((¬(p→q)→(q→¬(p→q)))→(¬(p→q)→¬q)) by detachment of [L1] and [L6]
[L8] (¬(p→q)→(q→¬(p→q))) by substitution of [A1] with p↦¬(p→q), q↦q
[L9] (¬(p→q)→¬q) by detachment of [L7] and [L8]

Proof by Tableau method is here.