Axiomatic Proof Of p→(¬q→¬(p→q))
This theorem serves in proof of completenes of axiom system.
Axiomatic proof follows.
[L1] ((p→((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q))))→((p→(¬q→(((p→q)→¬q)→¬(p→q))))→(p→(¬q→¬(p→q))))) by substitution of [A2] with p↦p, q↦(¬q→(((p→q)→¬q)→¬(p→q))), r↦(¬q→¬(p→q)) [L2] (((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q)))→(p→((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q))))) by substitution of [A1] with p↦((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q))), q↦p [L3] (((¬q→(((p→q)→¬q)→¬(p→q)))→((¬q→((p→q)→¬q))→(¬q→¬(p→q))))→(((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→((p→q)→¬q)))→((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q))))) by substitution of [A2] with p↦(¬q→(((p→q)→¬q)→¬(p→q))), q↦(¬q→((p→q)→¬q)), r↦(¬q→¬(p→q)) [L4] ((¬q→(((p→q)→¬q)→¬(p→q)))→((¬q→((p→q)→¬q))→(¬q→¬(p→q)))) by substitution of [A2] with p↦¬q, q↦((p→q)→¬q), r↦¬(p→q) [L5] (((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→((p→q)→¬q)))→((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q)))) by detachment of [L3] and [L4] [L6] ((¬q→((p→q)→¬q))→((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→((p→q)→¬q)))) by substitution of [A1] with p↦(¬q→((p→q)→¬q)), q↦(¬q→(((p→q)→¬q)→¬(p→q))) [L7] (¬q→((p→q)→¬q)) by substitution of [A1] with p↦¬q, q↦(p→q) [L8] ((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→((p→q)→¬q))) by detachment of [L6] and [L7] [L9] ((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q))) by detachment of [L5] and [L8] [L10] (p→((¬q→(((p→q)→¬q)→¬(p→q)))→(¬q→¬(p→q)))) by detachment of [L2] and [L9] [L11] ((p→(¬q→(((p→q)→¬q)→¬(p→q))))→(p→(¬q→¬(p→q)))) by detachment of [L1] and [L10] [L12] ((p→((((p→q)→¬q)→¬(p→q))→(¬q→(((p→q)→¬q)→¬(p→q)))))→((p→(((p→q)→¬q)→¬(p→q)))→(p→(¬q→(((p→q)→¬q)→¬(p→q)))))) by substitution of [A2] with p↦p, q↦(((p→q)→¬q)→¬(p→q)), r↦(¬q→(((p→q)→¬q)→¬(p→q))) [L13] (((((p→q)→¬q)→¬(p→q))→(¬q→(((p→q)→¬q)→¬(p→q))))→(p→((((p→q)→¬q)→¬(p→q))→(¬q→(((p→q)→¬q)→¬(p→q)))))) by substitution of [A1] with p↦((((p→q)→¬q)→¬(p→q))→(¬q→(((p→q)→¬q)→¬(p→q)))), q↦p [L14] ((((p→q)→¬q)→¬(p→q))→(¬q→(((p→q)→¬q)→¬(p→q)))) by substitution of [A1] with p↦(((p→q)→¬q)→¬(p→q)), q↦¬q [L15] (p→((((p→q)→¬q)→¬(p→q))→(¬q→(((p→q)→¬q)→¬(p→q))))) by detachment of [L13] and [L14] [L16] ((p→(((p→q)→¬q)→¬(p→q)))→(p→(¬q→(((p→q)→¬q)→¬(p→q))))) by detachment of [L12] and [L15] [L17] ((p→(((p→q)→q)→(((p→q)→¬q)→¬(p→q))))→((p→((p→q)→q))→(p→(((p→q)→¬q)→¬(p→q))))) by substitution of [A2] with p↦p, q↦((p→q)→q), r↦(((p→q)→¬q)→¬(p→q)) [L18] ((((p→q)→q)→(((p→q)→¬q)→¬(p→q)))→(p→(((p→q)→q)→(((p→q)→¬q)→¬(p→q))))) by substitution of [A1] with p↦(((p→q)→q)→(((p→q)→¬q)→¬(p→q))), q↦p [L19] (((p→q)→q)→(((p→q)→¬q)→¬(p→q))) by substitution of [A9] with p↦(p→q), q↦q [L20] (p→(((p→q)→q)→(((p→q)→¬q)→¬(p→q)))) by detachment of [L18] and [L19] [L21] ((p→((p→q)→q))→(p→(((p→q)→¬q)→¬(p→q)))) by detachment of [L17] and [L20] [L22] ((p→(((p→q)→p)→((p→q)→q)))→((p→((p→q)→p))→(p→((p→q)→q)))) by substitution of [A2] with p↦p, q↦((p→q)→p), r↦((p→q)→q) [L23] ((((p→q)→p)→((p→q)→q))→(p→(((p→q)→p)→((p→q)→q)))) by substitution of [A1] with p↦(((p→q)→p)→((p→q)→q)), q↦p [L24] (((p→q)→(p→q))→(((p→q)→p)→((p→q)→q))) by substitution of [A2] with p↦(p→q), q↦p, r↦q [L25] (((p→q)→((a→(p→q))→(p→q)))→(((p→q)→(a→(p→q)))→((p→q)→(p→q)))) by substitution of [A2] with p↦(p→q), q↦(a→(p→q)), r↦(p→q) [L26] ((p→q)→((a→(p→q))→(p→q))) by substitution of [A1] with p↦(p→q), q↦(a→(p→q)) [L27] (((p→q)→(a→(p→q)))→((p→q)→(p→q))) by detachment of [L25] and [L26] [L28] ((p→q)→(a→(p→q))) by substitution of [A1] with p↦(p→q), q↦a [L29] ((p→q)→(p→q)) by detachment of [L27] and [L28] [L30] (((p→q)→p)→((p→q)→q)) by detachment of [L24] and [L29] [L31] (p→(((p→q)→p)→((p→q)→q))) by detachment of [L23] and [L30] [L32] ((p→((p→q)→p))→(p→((p→q)→q))) by detachment of [L22] and [L31] [L33] (p→((p→q)→p)) by substitution of [A1] with p↦p, q↦(p→q) [L34] (p→((p→q)→q)) by detachment of [L32] and [L33] [L35] (p→(((p→q)→¬q)→¬(p→q))) by detachment of [L21] and [L34] [L36] (p→(¬q→(((p→q)→¬q)→¬(p→q)))) by detachment of [L16] and [L35] [L37] (p→(¬q→¬(p→q))) by detachment of [L11] and [L36]
Proof by Tableau method is here.