Theorem 2sbbid

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

	Ref	Expression
Hypotheses	sbbid.1	⊢ Ⅎ 𝑥 𝜑
	sbbid.2	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
	2sbbid.1	⊢ Ⅎ 𝑦 𝜑
Assertion	2sbbid	⊢ ( 𝜑 → ( [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sbbid.1	⊢ Ⅎ 𝑥 𝜑
2		sbbid.2	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
3		2sbbid.1	⊢ Ⅎ 𝑦 𝜑
4	3 2	sbbid	⊢ ( 𝜑 → ( [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑢 / 𝑦 ] 𝜒 ) )
5	1 4	sbbid	⊢ ( 𝜑 → ( [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑡 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 ) )