Theorem 2sbievw

Description: 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 Gino Giotto, 10-Jan-2024)

	Ref	Expression
Hypothesis	2sbievw.1	$$⊢\left(x=t\wedge y=u\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	2sbievw	$$⊢\left[t/x\right]\left[u/y\right]\phi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		2sbievw.1	$$⊢\left(x=t\wedge y=u\right)\to \left(\phi \leftrightarrow \psi \right)$$
2	1	sbiedvw	$$⊢x=t\to \left(\left[u/y\right]\phi \leftrightarrow \psi \right)$$
3	2	sbievw	$$⊢\left[t/x\right]\left[u/y\right]\phi \leftrightarrow \psi$$