Axiomatic Proof Of Implication Transposition
These two formulas are present in Whitehead/Russel Principia Mathematica.
Axiomatic proofs follow.
[L1] (((p→q)→((¬q→((p→¬q)→¬p))→(¬q→¬p)))→(((p→q)→(¬q→((p→¬q)→¬p)))→((p→q)→(¬q→¬p)))) by substitution of [A2] with p↦(p→q), q↦(¬q→((p→¬q)→¬p)), r↦(¬q→¬p) [L2] (((¬q→((p→¬q)→¬p))→(¬q→¬p))→((p→q)→((¬q→((p→¬q)→¬p))→(¬q→¬p)))) by substitution of [A1] with p↦((¬q→((p→¬q)→¬p))→(¬q→¬p)), q↦(p→q) [L3] (((¬q→((p→¬q)→¬p))→((¬q→(p→¬q))→(¬q→¬p)))→(((¬q→((p→¬q)→¬p))→(¬q→(p→¬q)))→((¬q→((p→¬q)→¬p))→(¬q→¬p)))) by substitution of [A2] with p↦(¬q→((p→¬q)→¬p)), q↦(¬q→(p→¬q)), r↦(¬q→¬p) [L4] ((¬q→((p→¬q)→¬p))→((¬q→(p→¬q))→(¬q→¬p))) by substitution of [A2] with p↦¬q, q↦(p→¬q), r↦¬p [L5] (((¬q→((p→¬q)→¬p))→(¬q→(p→¬q)))→((¬q→((p→¬q)→¬p))→(¬q→¬p))) by detachment of [L3] and [L4] [L6] ((¬q→(p→¬q))→((¬q→((p→¬q)→¬p))→(¬q→(p→¬q)))) by substitution of [A1] with p↦(¬q→(p→¬q)), q↦(¬q→((p→¬q)→¬p)) [L7] (¬q→(p→¬q)) by substitution of [A1] with p↦¬q, q↦p [L8] ((¬q→((p→¬q)→¬p))→(¬q→(p→¬q))) by detachment of [L6] and [L7] [L9] ((¬q→((p→¬q)→¬p))→(¬q→¬p)) by detachment of [L5] and [L8] [L10] ((p→q)→((¬q→((p→¬q)→¬p))→(¬q→¬p))) by detachment of [L2] and [L9] [L11] (((p→q)→(¬q→((p→¬q)→¬p)))→((p→q)→(¬q→¬p))) by detachment of [L1] and [L10] [L12] (((p→q)→(((p→¬q)→¬p)→(¬q→((p→¬q)→¬p))))→(((p→q)→((p→¬q)→¬p))→((p→q)→(¬q→((p→¬q)→¬p))))) by substitution of [A2] with p↦(p→q), q↦((p→¬q)→¬p), r↦(¬q→((p→¬q)→¬p)) [L13] ((((p→¬q)→¬p)→(¬q→((p→¬q)→¬p)))→((p→q)→(((p→¬q)→¬p)→(¬q→((p→¬q)→¬p))))) by substitution of [A1] with p↦(((p→¬q)→¬p)→(¬q→((p→¬q)→¬p))), q↦(p→q) [L14] (((p→¬q)→¬p)→(¬q→((p→¬q)→¬p))) by substitution of [A1] with p↦((p→¬q)→¬p), q↦¬q [L15] ((p→q)→(((p→¬q)→¬p)→(¬q→((p→¬q)→¬p)))) by detachment of [L13] and [L14] [L16] (((p→q)→((p→¬q)→¬p))→((p→q)→(¬q→((p→¬q)→¬p)))) by detachment of [L12] and [L15] [L17] ((p→q)→(¬q→((p→¬q)→¬p))) by detachment of [L16] and [A9] [L18] ((p→q)→(¬q→¬p)) by detachment of [L11] and [L17]
Proof by Tableau method is here.
[L1] (((¬q→¬p)→((p→(¬q→¬p))→(p→q)))→(((¬q→¬p)→(p→(¬q→¬p)))→((¬q→¬p)→(p→q)))) by substitution of [A2] with p↦(¬q→¬p), q↦(p→(¬q→¬p)), r↦(p→q) [L2] (((p→(¬q→¬p))→(p→q))→((¬q→¬p)→((p→(¬q→¬p))→(p→q)))) by substitution of [A1] with p↦((p→(¬q→¬p))→(p→q)), q↦(¬q→¬p) [L3] ((p→((¬q→¬p)→q))→((p→(¬q→¬p))→(p→q))) by substitution of [A2] with p↦p, q↦(¬q→¬p), r↦q [L4] ((p→(((¬q→¬p)→¬¬q)→((¬q→¬p)→q)))→((p→((¬q→¬p)→¬¬q))→(p→((¬q→¬p)→q)))) by substitution of [A2] with p↦p, q↦((¬q→¬p)→¬¬q), r↦((¬q→¬p)→q) [L5] ((((¬q→¬p)→¬¬q)→((¬q→¬p)→q))→(p→(((¬q→¬p)→¬¬q)→((¬q→¬p)→q)))) by substitution of [A1] with p↦(((¬q→¬p)→¬¬q)→((¬q→¬p)→q)), q↦p [L6] (((¬q→¬p)→(¬¬q→q))→(((¬q→¬p)→¬¬q)→((¬q→¬p)→q))) by substitution of [A2] with p↦(¬q→¬p), q↦¬¬q, r↦q [L7] ((¬¬q→q)→((¬q→¬p)→(¬¬q→q))) by substitution of [A1] with p↦(¬¬q→q), q↦(¬q→¬p) [L8] ((¬¬q→((¬q→q)→q))→((¬¬q→(¬q→q))→(¬¬q→q))) by substitution of [A2] with p↦¬¬q, q↦(¬q→q), r↦q [L9] (((¬q→q)→q)→(¬¬q→((¬q→q)→q))) by substitution of [A1] with p↦((¬q→q)→q), q↦¬¬q [L10] (((¬q→q)→((q∨¬q)→q))→(((¬q→q)→(q∨¬q))→((¬q→q)→q))) by substitution of [A2] with p↦(¬q→q), q↦(q∨¬q), r↦q [L11] ((q→q)→((¬q→q)→((q∨¬q)→q))) by substitution of [A8] with p↦q, r↦q, q↦¬q [L12] ((q→((a→q)→q))→((q→(a→q))→(q→q))) by substitution of [A2] with p↦q, q↦(a→q), r↦q [L13] (q→((a→q)→q)) by substitution of [A1] with p↦q, q↦(a→q) [L14] ((q→(a→q))→(q→q)) by detachment of [L12] and [L13] [L15] (q→(a→q)) by substitution of [A1] with p↦q, q↦a [L16] (q→q) by detachment of [L14] and [L15] [L17] ((¬q→q)→((q∨¬q)→q)) by detachment of [L11] and [L16] [L18] (((¬q→q)→(q∨¬q))→((¬q→q)→q)) by detachment of [L10] and [L17] [L19] ((q∨¬q)→((¬q→q)→(q∨¬q))) by substitution of [A1] with p↦(q∨¬q), q↦(¬q→q) [L20] (q∨¬q) by substitution of [A11] with p↦q [L21] ((¬q→q)→(q∨¬q)) by detachment of [L19] and [L20] [L22] ((¬q→q)→q) by detachment of [L18] and [L21] [L23] (¬¬q→((¬q→q)→q)) by detachment of [L9] and [L22] [L24] ((¬¬q→(¬q→q))→(¬¬q→q)) by detachment of [L8] and [L23] [L25] (¬¬q→(¬q→q)) by substitution of [A10] with p↦¬q, q↦q [L26] (¬¬q→q) by detachment of [L24] and [L25] [L27] ((¬q→¬p)→(¬¬q→q)) by detachment of [L7] and [L26] [L28] (((¬q→¬p)→¬¬q)→((¬q→¬p)→q)) by detachment of [L6] and [L27] [L29] (p→(((¬q→¬p)→¬¬q)→((¬q→¬p)→q))) by detachment of [L5] and [L28] [L30] ((p→((¬q→¬p)→¬¬q))→(p→((¬q→¬p)→q))) by detachment of [L4] and [L29] [L31] ((p→((¬q→p)→((¬q→¬p)→¬¬q)))→((p→(¬q→p))→(p→((¬q→¬p)→¬¬q)))) by substitution of [A2] with p↦p, q↦(¬q→p), r↦((¬q→¬p)→¬¬q) [L32] (((¬q→p)→((¬q→¬p)→¬¬q))→(p→((¬q→p)→((¬q→¬p)→¬¬q)))) by substitution of [A1] with p↦((¬q→p)→((¬q→¬p)→¬¬q)), q↦p [L33] ((¬q→p)→((¬q→¬p)→¬¬q)) by substitution of [A9] with p↦¬q, q↦p [L34] (p→((¬q→p)→((¬q→¬p)→¬¬q))) by detachment of [L32] and [L33] [L35] ((p→(¬q→p))→(p→((¬q→¬p)→¬¬q))) by detachment of [L31] and [L34] [L36] (p→(¬q→p)) by substitution of [A1] with p↦p, q↦¬q [L37] (p→((¬q→¬p)→¬¬q)) by detachment of [L35] and [L36] [L38] (p→((¬q→¬p)→q)) by detachment of [L30] and [L37] [L39] ((p→(¬q→¬p))→(p→q)) by detachment of [L3] and [L38] [L40] ((¬q→¬p)→((p→(¬q→¬p))→(p→q))) by detachment of [L2] and [L39] [L41] (((¬q→¬p)→(p→(¬q→¬p)))→((¬q→¬p)→(p→q))) by detachment of [L1] and [L40] [L42] ((¬q→¬p)→(p→(¬q→¬p))) by substitution of [A1] with p↦(¬q→¬p), q↦p [L43] ((¬q→¬p)→(p→q)) by detachment of [L41] and [L42]
Proof by Tableau method is here.