Description: Conversion of double implicit substitution to explicit substitution.
Usage of this theorem is discouraged because it depends on ax-13 .
See 2sbievw for a version with extra disjoint variables, but based on
fewer axioms. (Contributed by AV, 29-Jul-2023)(New usage is discouraged.)