Description: Obsolete version of sbt as of 6-Jul-2023. A substitution into a
theorem yields a theorem. See sbt when x , y need not be
disjoint. (Contributed by BJ, 31-May-2019) Reduce axioms. (Revised by Steven Nguyen, 25-Apr-2023)(New usage is discouraged.)(Proof modification is discouraged.)