assignb reduces the assignment [x:=e]p(x) to p(e), because p is true of x after assigning e to x if and only if p is true of the new value e that will be assigned to x.

Other tactics such as chase and unfold also use this axiom.