Description: Obsolete version of sbim as of 24-Jul-2023. Substitution distributes
over implication. Version of sbim with a disjoint variable condition,
not requiring ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023)(New usage is discouraged.)(Proof modification is discouraged.)