Theorem 2sbiev

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

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

Proof

Step	Hyp	Ref	Expression
1		2sbiev.1	$$⊢\left(x=t\wedge y=u\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		nfv	$$⊢Ⅎx\psi$$
3	1	sbiedv	$$⊢x=t\to \left(\left[u/y\right]\phi \leftrightarrow \psi \right)$$
4	2 3	sbie	$$⊢\left[t/x\right]\left[u/y\right]\phi \leftrightarrow \psi$$