Axiomatic Proof Of Material Implication

These two formulas are present in Whitehead/Russel Principia Mathematica.

Axiomatic proofs follow.

[L1] (((p→(q→(¬p∨q)))→(((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q))))→(((p→(q→(¬p∨q)))→((p→q)→(p→(¬p∨q))))→((p→(q→(¬p∨q)))→((p→q)→(¬p∨q))))) by substitution of [A2] with p↦(p→(q→(¬p∨q))), q↦((p→q)→(p→(¬p∨q))), r↦((p→q)→(¬p∨q))
[L2] ((((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q)))→((p→(q→(¬p∨q)))→(((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q))))) by substitution of [A1] with p↦(((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q))), q↦(p→(q→(¬p∨q)))
[L3] (((p→q)→((p→(¬p∨q))→(¬p∨q)))→(((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q)))) by substitution of [A2] with p↦(p→q), q↦(p→(¬p∨q)), r↦(¬p∨q)
[L4] (((p→(¬p∨q))→(¬p∨q))→((p→q)→((p→(¬p∨q))→(¬p∨q)))) by substitution of [A1] with p↦((p→(¬p∨q))→(¬p∨q)), q↦(p→q)
[L5] (((p→(¬p∨q))→((¬p∨p)→(¬p∨q)))→(((p→(¬p∨q))→(¬p∨p))→((p→(¬p∨q))→(¬p∨q)))) by substitution of [A2] with p↦(p→(¬p∨q)), q↦(¬p∨p), r↦(¬p∨q)
[L6] ((¬p→(¬p∨q))→((p→(¬p∨q))→((¬p∨p)→(¬p∨q)))) by substitution of [A8] with p↦¬p, r↦(¬p∨q), q↦p
[L7] (¬p→(¬p∨q)) by substitution of [A6] with p↦¬p, q↦q
[L8] ((p→(¬p∨q))→((¬p∨p)→(¬p∨q))) by detachment of [L6] and [L7]
[L9] (((p→(¬p∨q))→(¬p∨p))→((p→(¬p∨q))→(¬p∨q))) by detachment of [L5] and [L8]
[L10] ((¬p∨p)→((p→(¬p∨q))→(¬p∨p))) by substitution of [A1] with p↦(¬p∨p), q↦(p→(¬p∨q))
[L11] ((p→(¬p∨p))→((¬p→(¬p∨p))→((p∨¬p)→(¬p∨p)))) by substitution of [A8] with p↦p, r↦(¬p∨p), q↦¬p
[L12] (p→(¬p∨p)) by substitution of [A7] with q↦p, p↦¬p
[L13] ((¬p→(¬p∨p))→((p∨¬p)→(¬p∨p))) by detachment of [L11] and [L12]
[L14] (¬p→(¬p∨p)) by substitution of [A6] with p↦¬p, q↦p
[L15] ((p∨¬p)→(¬p∨p)) by detachment of [L13] and [L14]
[L16] (¬p∨p) by detachment of [L15] and [A11]
[L17] ((p→(¬p∨q))→(¬p∨p)) by detachment of [L10] and [L16]
[L18] ((p→(¬p∨q))→(¬p∨q)) by detachment of [L9] and [L17]
[L19] ((p→q)→((p→(¬p∨q))→(¬p∨q))) by detachment of [L4] and [L18]
[L20] (((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q))) by detachment of [L3] and [L19]
[L21] ((p→(q→(¬p∨q)))→(((p→q)→(p→(¬p∨q)))→((p→q)→(¬p∨q)))) by detachment of [L2] and [L20]
[L22] (((p→(q→(¬p∨q)))→((p→q)→(p→(¬p∨q))))→((p→(q→(¬p∨q)))→((p→q)→(¬p∨q)))) by detachment of [L1] and [L21]
[L23] ((p→(q→(¬p∨q)))→((p→q)→(p→(¬p∨q)))) by substitution of [A2] with p↦p, q↦q, r↦(¬p∨q)
[L24] ((p→(q→(¬p∨q)))→((p→q)→(¬p∨q))) by detachment of [L22] and [L23]
[L25] ((q→(¬p∨q))→(p→(q→(¬p∨q)))) by substitution of [A1] with p↦(q→(¬p∨q)), q↦p
[L26] (q→(¬p∨q)) by substitution of [A7] with q↦q, p↦¬p
[L27] (p→(q→(¬p∨q))) by detachment of [L25] and [L26]
[L28] ((p→q)→(¬p∨q)) by detachment of [L24] and [L27]

Proof by Tableau method is here.

[L1] ((¬p→(p→q))→((q→(p→q))→((¬p∨q)→(p→q)))) by substitution of [A8] with p↦¬p, r↦(p→q), q↦q
[L2] ((q→(p→q))→((¬p∨q)→(p→q))) by detachment of [L1] and [A10]
[L3] (q→(p→q)) by substitution of [A1] with p↦q, q↦p
[L4] ((¬p∨q)→(p→q)) by detachment of [L2] and [L3]

Proof by Tableau method is here.