Axiomatic Proof Of Disjunction's Commutativity Law

Law of Commutativity Of Disjunction is important in logic.

I provide an axiomatic proof.

[L1] (p→(q∨p)) by substituton of [A7] with q↦p, p↦q
[L2] (q→(q∨p)) by substituton of [A6] with p↦q, q↦p
[L3] ((p→(q∨p))→((q→(q∨p))→((p∨q)→(q∨p)))) by substituton of [A8] with p↦p, r↦(q∨p), q↦q
[L4] ((q→(q∨p))→((p∨q)→(q∨p))) by detachment of [L3] and [L1]
[L5] ((p∨q)→(q∨p)) by detachment of [L4] and [L2]

Proof by Tableau method is here.