Description: Equivalence for substitution when y is not free in ph . The
implication "to the right" is sb1 and does not require the
non-freeness hypothesis. Theorem sb5 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, 5-Aug-1993)(Revised by Mario Carneiro, 4-Oct-2016)(New usage is discouraged.)