A or B = B or A proof (natural deduction)

This problem feels like it should be simpler than I've made it so my ultimate question will be: is there a simpler way to do this? In logic we know that

A v B = B v A

But in natural deduction we use our v-Introductions, RAA, etc. to prove these equivalences. In the process of solving a practice problem, I encountered the need to prove this commutative property but am finding it surprisingly difficult. It seems to me that the proof will start out like this:

1. A v B            given
2.     ¬(B v A)     assume
3.     ¬B ^ ¬A      2, deMorgan's
4.     ¬A           3, ^-elimination
5.     ¬B           3, ^-elimination
6.     ¬A ^ ¬B      4, 5, ^-I
7.     ¬(A v B)     6, deMorgan's
?. B v A            2, 7 RAA

And now we find ourselves in a position where we must prove deMorgan's. Is there no simpler proof for A v B = B v A?

The following proof used Klement's proof checker. Additional information can be found in the forallx text. Links to both are below.

Disjunction introduction (∨I) allows one to rebuild the disjunction in a different order.

One finishes the proof with the final line using disjunction elimination (∨E) referencing the disjunction itself (line 1), the first disjunct subproof (lines 2-3) reaching the desired result and the second disjunct subproof (lines 4-5) arriving at the desired result.

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/