Description: Conversion of implicit substitution to explicit substitution (deduction
version of sbie ). Usage of this theorem is discouraged because it
depends on ax-13 . Use the weaker sbiedvw when possible.
(Contributed by NM, 7-Jan-2017)(New usage is discouraged.)