Theorem 2sbbii

Description: Infer double substitution into both sides of a logical equivalence. (Contributed by AV, 30-Jul-2023)

	Ref	Expression
Hypothesis	sbbii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	2sbbii	$$⊢\left[t/x\right]\left[u/y\right]\phi \leftrightarrow \left[t/x\right]\left[u/y\right]\psi$$

Proof

Step	Hyp	Ref	Expression
1		sbbii.1	$$⊢\phi \leftrightarrow \psi$$
2	1	sbbii	$$⊢\left[u/y\right]\phi \leftrightarrow \left[u/y\right]\psi$$
3	2	sbbii	$$⊢\left[t/x\right]\left[u/y\right]\phi \leftrightarrow \left[t/x\right]\left[u/y\right]\psi$$