Axiomatic Proof Of Implication Contraposition
These two formulas are present in Whitehead/Russel Principia Mathematica.
Axiomatic proofs follow.
[L1] (((¬p→q)→((p∨¬p)→(¬q→p)))→(((¬p→q)→(p∨¬p))→((¬p→q)→(¬q→p)))) by substitution of [A2] with p↦(¬p→q), q↦(p∨¬p), r↦(¬q→p) [L2] (((¬p→q)→((¬p→(¬q→p))→((p∨¬p)→(¬q→p))))→(((¬p→q)→(¬p→(¬q→p)))→((¬p→q)→((p∨¬p)→(¬q→p))))) by substitution of [A2] with p↦(¬p→q), q↦(¬p→(¬q→p)), r↦((p∨¬p)→(¬q→p)) [L3] (((¬p→(¬q→p))→((p∨¬p)→(¬q→p)))→((¬p→q)→((¬p→(¬q→p))→((p∨¬p)→(¬q→p))))) by substitution of [A1] with p↦((¬p→(¬q→p))→((p∨¬p)→(¬q→p))), q↦(¬p→q) [L4] ((p→(¬q→p))→((¬p→(¬q→p))→((p∨¬p)→(¬q→p)))) by substitution of [A8] with p↦p, r↦(¬q→p), q↦¬p [L5] (p→(¬q→p)) by substitution of [A1] with p↦p, q↦¬q [L6] ((¬p→(¬q→p))→((p∨¬p)→(¬q→p))) by detachment of [L4] and [L5] [L7] ((¬p→q)→((¬p→(¬q→p))→((p∨¬p)→(¬q→p)))) by detachment of [L3] and [L6] [L8] (((¬p→q)→(¬p→(¬q→p)))→((¬p→q)→((p∨¬p)→(¬q→p)))) by detachment of [L2] and [L7] [L9] ((¬p→(q→(¬q→p)))→((¬p→q)→(¬p→(¬q→p)))) by substitution of [A2] with p↦¬p, q↦q, r↦(¬q→p) [L10] ((q→(¬q→p))→(¬p→(q→(¬q→p)))) by substitution of [A1] with p↦(q→(¬q→p)), q↦¬p [L11] ((q→((¬q→q)→(¬q→p)))→((q→(¬q→q))→(q→(¬q→p)))) by substitution of [A2] with p↦q, q↦(¬q→q), r↦(¬q→p) [L12] (((¬q→q)→(¬q→p))→(q→((¬q→q)→(¬q→p)))) by substitution of [A1] with p↦((¬q→q)→(¬q→p)), q↦q [L13] ((¬q→(q→p))→((¬q→q)→(¬q→p))) by substitution of [A2] with p↦¬q, q↦q, r↦p [L14] (¬q→(q→p)) by substitution of [A10] with p↦q, q↦p [L15] ((¬q→q)→(¬q→p)) by detachment of [L13] and [L14] [L16] (q→((¬q→q)→(¬q→p))) by detachment of [L12] and [L15] [L17] ((q→(¬q→q))→(q→(¬q→p))) by detachment of [L11] and [L16] [L18] (q→(¬q→q)) by substitution of [A1] with p↦q, q↦¬q [L19] (q→(¬q→p)) by detachment of [L17] and [L18] [L20] (¬p→(q→(¬q→p))) by detachment of [L10] and [L19] [L21] ((¬p→q)→(¬p→(¬q→p))) by detachment of [L9] and [L20] [L22] ((¬p→q)→((p∨¬p)→(¬q→p))) by detachment of [L8] and [L21] [L23] (((¬p→q)→(p∨¬p))→((¬p→q)→(¬q→p))) by detachment of [L1] and [L22] [L24] ((p∨¬p)→((¬p→q)→(p∨¬p))) by substitution of [A1] with p↦(p∨¬p), q↦(¬p→q) [L25] ((¬p→q)→(p∨¬p)) by detachment of [L24] and [A11] [L26] ((¬p→q)→(¬q→p)) by detachment of [L23] and [L25]
Proof by Tableau method is here.
[L1] (((p→¬q)→((q→(p→¬q))→(q→¬p)))→(((p→¬q)→(q→(p→¬q)))→((p→¬q)→(q→¬p)))) by substitution of [A2] with p↦(p→¬q), q↦(q→(p→¬q)), r↦(q→¬p) [L2] (((q→(p→¬q))→(q→¬p))→((p→¬q)→((q→(p→¬q))→(q→¬p)))) by substitution of [A1] with p↦((q→(p→¬q))→(q→¬p)), q↦(p→¬q) [L3] ((q→((p→¬q)→¬p))→((q→(p→¬q))→(q→¬p))) by substitution of [A2] with p↦q, q↦(p→¬q), r↦¬p [L4] ((q→((p→q)→((p→¬q)→¬p)))→((q→(p→q))→(q→((p→¬q)→¬p)))) by substitution of [A2] with p↦q, q↦(p→q), r↦((p→¬q)→¬p) [L5] (((p→q)→((p→¬q)→¬p))→(q→((p→q)→((p→¬q)→¬p)))) by substitution of [A1] with p↦((p→q)→((p→¬q)→¬p)), q↦q [L6] (q→((p→q)→((p→¬q)→¬p))) by detachment of [L5] and [A9] [L7] ((q→(p→q))→(q→((p→¬q)→¬p))) by detachment of [L4] and [L6] [L8] (q→(p→q)) by substitution of [A1] with p↦q, q↦p [L9] (q→((p→¬q)→¬p)) by detachment of [L7] and [L8] [L10] ((q→(p→¬q))→(q→¬p)) by detachment of [L3] and [L9] [L11] ((p→¬q)→((q→(p→¬q))→(q→¬p))) by detachment of [L2] and [L10] [L12] (((p→¬q)→(q→(p→¬q)))→((p→¬q)→(q→¬p))) by detachment of [L1] and [L11] [L13] ((p→¬q)→(q→(p→¬q))) by substitution of [A1] with p↦(p→¬q), q↦q [L14] ((p→¬q)→(q→¬p)) by detachment of [L12] and [L13]
Proof by Tableau method is here.