Theorem 2sbbii

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

	Ref	Expression
Hypothesis	sbbii.1	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	2sbbii	⊢ ( [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2	1	sbbii	⊢ ( [ 𝑢 / 𝑦 ] 𝜑 ↔ [ 𝑢 / 𝑦 ] 𝜓 )
3	2	sbbii	⊢ ( [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )