Substituting \( y \) for \( x \) and then \( z' \) for \( y \) is equivalent to substituting \( z' \) for both \( x \) and \( y \). Version of sbcom3 with a disjoint variable condition using fewer axioms. (Contributed by NM, 27-May-1997.) (Revised by Giovanni Mascellani, 8-Apr-2018.) (Revised by BJ, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 19-Jan-2023.)