Theorem 2sbiev

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.)

Hypothesis
2sbiev.1
\( \vdash x = t' \wedge y = u' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash [ t' / x ] \, [ u' / y ] \, \varphi \leftrightarrow \psi \)
Proof
l0
nfv
2sbiev.1
sbiedv _
sbie l0 _