Axiomatic Proof Of Conjunction's Commutativity Law

Law of Commutativity Of Conjunction is one of the main building bricks in logic.

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

[L1] ((p∧q)→p) by substituton of [A3] with p↦p, q↦q
[L2] ((p∧q)→q) by substituton of [A4] with p↦p, q↦q
[L3] (q→(p→(q∧p))) by substituton of [A5] with p↦q, q↦p
[L4] ((q→(p→(q∧p)))→((p∧q)→(q→(p→(q∧p))))) by substituton of [A1] with p↦(q→(p→(q∧p))), q↦(p∧q)
[L5] (((p∧q)→(p→(q∧p)))→(((p∧q)→p)→((p∧q)→(q∧p)))) by substituton of [A2] with p↦(p∧q), q↦p, r↦(q∧p)
[L6] (((p∧q)→(q→(p→(q∧p))))→(((p∧q)→q)→((p∧q)→(p→(q∧p))))) by substituton of [A2] with p↦(p∧q), q↦q, r↦(p→(q∧p))
[L7] ((p∧q)→(q→(p→(q∧p)))) by detachment of [L4] and [L3]
[L8] (((p∧q)→q)→((p∧q)→(p→(q∧p)))) by detachment of [L6] and [L7]
[L9] ((p∧q)→(p→(q∧p))) by detachment of [L8] and [L2]
[L10] (((p∧q)→p)→((p∧q)→(q∧p))) by detachment of [L5] and [L9]
[L11] ((p∧q)→(q∧p)) by detachment of [L10] and [L1]

Proof by Tableau method is here.