Description: If z is not free in ph , it is not free in [ y / x ] ph when
z is distinct from x and y . Version of nfsb requiring
more disjoint variables, but fewer axioms. (Contributed by Mario
Carneiro, 11-Aug-2016)(Revised by Wolf Lammen, 7-Feb-2023) Remove
disjoint variable condition on x , y . (Revised by Steven Nguyen, 13-Aug-2023)