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.
[x:=e]p(x)
p(e)
p
x
e
Other tactics such as chase and unfold also use this axiom.