Theorem breq123d

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011)

	Ref	Expression
Hypotheses	breq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	breq123d.2	⊢ ( 𝜑 → 𝑅 = 𝑆 )
	breq123d.3	⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion	breq123d	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑆 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		breq1d.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		breq123d.2	⊢ ( 𝜑 → 𝑅 = 𝑆 )
3		breq123d.3	⊢ ( 𝜑 → 𝐶 = 𝐷 )
4	1 3	breq12d	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐷 ) )
5	2	breqd	⊢ ( 𝜑 → ( 𝐵 𝑅 𝐷 ↔ 𝐵 𝑆 𝐷 ) )
6	4 5	bitrd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑆 𝐷 ) )