Description: Equivalence for substitution when y is not free in ph . The
implication "to the left" is sb2 and does not require the non-freeness
hypothesis. Theorem sb6 replaces the non-freeness hypothesis with a
disjoint variable condition and uses less axioms. Usage of this theorem
is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jun-1993)(Revised by Mario Carneiro, 4-Oct-2016)(New usage is discouraged.)