Theorem 2sbbid

Description: Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023)

	Ref	Expression
Hypotheses	sbbid.1	$$⊢Ⅎx\phi$$
	sbbid.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
	2sbbid.1	$$⊢Ⅎy\phi$$
Assertion	2sbbid	$$⊢\phi \to \left(\left[t/x\right]\left[u/y\right]\psi \leftrightarrow \left[t/x\right]\left[u/y\right]\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbbid.1	$$⊢Ⅎx\phi$$
2		sbbid.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
3		2sbbid.1	$$⊢Ⅎy\phi$$
4	3 2	sbbid	$$⊢\phi \to \left(\left[u/y\right]\psi \leftrightarrow \left[u/y\right]\chi \right)$$
5	1 4	sbbid	$$⊢\phi \to \left(\left[t/x\right]\left[u/y\right]\psi \leftrightarrow \left[t/x\right]\left[u/y\right]\chi \right)$$