You can perform the universal quantification of variables in any order since it is commutative. Recall that the definition of universal quantification is ∀x.φ := φ[x:=0] ⋀ φ[x:=1]. Thus, we have

- ∀x.∀y.φ = (∀y.φ)[x:=0] ⋀ (∀y.φ)[x:=1] = φ[x:=0][y:=0] ⋀ φ[x:=0][y:=1] ⋀ φ[x:=1][y:=0] ⋀ φ[x:=1][y:=1]
- ∀y.∀x.φ = (∀x.φ)[y:=0] ⋀ (∀x.φ)[y:=1] = φ[x:=0][y:=0] ⋀ φ[x:=1][y:=0] ⋀ φ[x:=0][y:=1] ⋀ φ[x:=1][y:=1]

which are the same (note that φ[x:=0][y:=1] and φ[y:=1][x:=0] are the same: what we do is replacing occurrences of x and y by 0 and since occurrences of x are not occurrences of y, the two are not in conflict).

Hence, we have ∀x.∀y.φ = ∀y.∀x.φ, and by negation, we also see that ∃x.∃y.φ = ∃y.∃x.φ holds. However, you cannot change the order of alternating quantifiers like ∀x.∃y.φ or ∃x.∀y.φ.

And you are right with your observation that you can often significantly save work when you choose that variable first that will reduce the formula as much as possible since one part φ[x:=0] or φ[x:=1] may be just true or a small formula.