Description: A composition law for substitution. For versions requiring fewer
axioms, but more disjoint variable conditions, see sbco2v and
sbco2vv . Usage of this theorem is discouraged because it depends on
ax-13 . (Contributed by NM, 30-Jun-1994)(Revised by Mario
Carneiro, 6-Oct-2016)(Proof shortened by Wolf Lammen, 17-Sep-2018)(New usage is discouraged.)