Theorem sbrbif

Description: Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993) (Revised by Mario Carneiro, 4-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		sbrbif.1	⊢ Ⅎ 𝑥 𝜒
2		sbrbif.2	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
3	2	sbrbis	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) )
4	1	sbf	⊢ ( [ 𝑦 / 𝑥 ] 𝜒 ↔ 𝜒 )
5	4	bibi2i	⊢ ( ( 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) )
6	3 5	bitri	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) )