This rule is needed, in particular, to derive commutativity of disjunction. Indeed, suppose (p or q). We are reasoning by cases. If p, then (q or p) by addition. Similarly, if q, then again (q or p). Since in both cases we have the same conclusion, this conclusion follows from (p or q).