Theorem 2sbievw

Conversion of double implicit substitution to explicit substitution. Version of 2sbiev with more disjoint variable conditions, requiring fewer axioms. (Contributed by AV, 29-Jul-2023.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)

Hypothesis

2sbievw.1

\( \vdash x = t' \wedge y = u' \rightarrow (\varphi \leftrightarrow \psi) \)

Conclusion

\( \vdash [ t' / x ] \, [ u' / y ] \, \varphi \leftrightarrow \psi \)

Proof

2sbievw.1

sbiedvw _

sbievw _