Description: Obsolete version of sbi1 as of 24-Jul-2023. Removal of implication from substitution. (Contributed by NM, 14-May-1993) (New usage is discouraged.) (Proof modification is discouraged.)