Description: Obsolete version of sblbis as of 24-Jul-2023. Introduce left
biconditional inside of a substitution. Version of sblbis with a
disjoint variable condition, not requiring ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023)(New usage is discouraged.)(Proof modification is discouraged.)