Description: Obsolete version of spsbim as of 6-Jul-2023. Specialization of
implication. Version of spsbim with a disjoint variable condition,
not requiring ax-13 . (Contributed by Wolf Lammen, 19-Jan-2023)(New usage is discouraged.)(Proof modification is discouraged.)