Axiomatic Proof Of Peirce's Law

Peirce's Law is a very short statement that is true, but hard to understand by heart.

Usually it is proven using Deduction Theorem. Here I provide an axiomatic proof.

[L1] ((¬((p→q)→p)→(((p→q)→p)→p))→((((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(((p→q)→p)→p))→((¬((p→q)→p)∨((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))))→(((p→q)→p)→p)))) by substitution of [A8] with p↦¬((p→q)→p), r↦(((p→q)→p)→p), q↦((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))
[L2] (¬((p→q)→p)→(((p→q)→p)→p)) by substitution of [A10] with p↦((p→q)→p), q↦p
[L3] ((((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(((p→q)→p)→p))→((¬((p→q)→p)∨((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))))→(((p→q)→p)→p))) by detachment of [L1] and [L2]
[L4] ((((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→((p∨¬p)→(((p→q)→p)→p)))→((((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(p∨¬p))→(((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(((p→q)→p)→p)))) by substitution of [A2] with p↦((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))), q↦(p∨¬p), r↦(((p→q)→p)→p)
[L5] (((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→((p∨¬p)→(((p→q)→p)→p))) by substitution of [A4] with p↦(p∨¬p), q↦((p∨¬p)→(((p→q)→p)→p))
[L6] ((((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(p∨¬p))→(((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(((p→q)→p)→p))) by detachment of [L4] and [L5]
[L7] (((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(p∨¬p)) by substitution of [A3] with p↦(p∨¬p), q↦((p∨¬p)→(((p→q)→p)→p))
[L8] (((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(((p→q)→p)→p)) by detachment of [L6] and [L7]
[L9] ((¬((p→q)→p)∨((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))))→(((p→q)→p)→p)) by detachment of [L3] and [L8]
[L10] (((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))→(¬((p→q)→p)∨((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))))) by substitution of [A7] with q↦((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))), p↦¬((p→q)→p)
[L11] ((p∨¬p)→(((p∨¬p)→(((p→q)→p)→p))→((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))))) by substitution of [A5] with p↦(p∨¬p), q↦((p∨¬p)→(((p→q)→p)→p))
[L12] (((p∨¬p)→(((p→q)→p)→p))→((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))) by detachment of [L11] and [A11]
[L13] ((p→(((p→q)→p)→p))→((¬p→(((p→q)→p)→p))→((p∨¬p)→(((p→q)→p)→p)))) by substitution of [A8] with p↦p, r↦(((p→q)→p)→p), q↦¬p
[L14] (p→(((p→q)→p)→p)) by substitution of [A1] with p↦p, q↦((p→q)→p)
[L15] ((¬p→(((p→q)→p)→p))→((p∨¬p)→(((p→q)→p)→p))) by detachment of [L13] and [L14]
[L16] ((¬p→((((p→q)→p)→(p→q))→(((p→q)→p)→p)))→((¬p→(((p→q)→p)→(p→q)))→(¬p→(((p→q)→p)→p)))) by substitution of [A2] with p↦¬p, q↦(((p→q)→p)→(p→q)), r↦(((p→q)→p)→p)
[L17] (((((p→q)→p)→(p→q))→(((p→q)→p)→p))→(¬p→((((p→q)→p)→(p→q))→(((p→q)→p)→p)))) by substitution of [A1] with p↦((((p→q)→p)→(p→q))→(((p→q)→p)→p)), q↦¬p
[L18] ((((p→q)→p)→((p→q)→p))→((((p→q)→p)→(p→q))→(((p→q)→p)→p))) by substitution of [A2] with p↦((p→q)→p), q↦(p→q), r↦p
[L19] (((p→q)→(p→p))→(((p→q)→p)→((p→q)→p))) by substitution of [A2] with p↦(p→q), q↦p, r↦p
[L20] ((p→(q→p))→((p→q)→(p→p))) by substitution of [A2] with p↦p, q↦q, r↦p
[L21] ((p→q)→(p→p)) by detachment of [L20] and [A1]
[L22] (((p→q)→p)→((p→q)→p)) by detachment of [L19] and [L21]
[L23] ((((p→q)→p)→(p→q))→(((p→q)→p)→p)) by detachment of [L18] and [L22]
[L24] (¬p→((((p→q)→p)→(p→q))→(((p→q)→p)→p))) by detachment of [L17] and [L23]
[L25] ((¬p→(((p→q)→p)→(p→q)))→(¬p→(((p→q)→p)→p))) by detachment of [L16] and [L24]
[L26] ((¬p→((p→q)→(((p→q)→p)→(p→q))))→((¬p→(p→q))→(¬p→(((p→q)→p)→(p→q))))) by substitution of [A2] with p↦¬p, q↦(p→q), r↦(((p→q)→p)→(p→q))
[L27] (((p→q)→(((p→q)→p)→(p→q)))→(¬p→((p→q)→(((p→q)→p)→(p→q))))) by substitution of [A1] with p↦((p→q)→(((p→q)→p)→(p→q))), q↦¬p
[L28] ((p→q)→(((p→q)→p)→(p→q))) by substitution of [A1] with p↦(p→q), q↦((p→q)→p)
[L29] (¬p→((p→q)→(((p→q)→p)→(p→q)))) by detachment of [L27] and [L28]
[L30] ((¬p→(p→q))→(¬p→(((p→q)→p)→(p→q)))) by detachment of [L26] and [L29]
[L31] (¬p→(((p→q)→p)→(p→q))) by detachment of [L30] and [A10]
[L32] (¬p→(((p→q)→p)→p)) by detachment of [L25] and [L31]
[L33] ((p∨¬p)→(((p→q)→p)→p)) by detachment of [L15] and [L32]
[L34] ((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p))) by detachment of [L12] and [L33]
[L35] (¬((p→q)→p)∨((p∨¬p)∧((p∨¬p)→(((p→q)→p)→p)))) by detachment of [L10] and [L34]
[L36] (((p→q)→p)→p) by detachment of [L9] and [L35]

Proof by Tableau method is here.