Theorem 3brtr3i

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999)

	Ref	Expression
Hypotheses	3brtr3.1	⊢ 𝐴 𝑅 𝐵
	3brtr3.2	⊢ 𝐴 = 𝐶
	3brtr3.3	⊢ 𝐵 = 𝐷
Assertion	3brtr3i	⊢ 𝐶 𝑅 𝐷

Proof

Step	Hyp	Ref	Expression
1		3brtr3.1	⊢ 𝐴 𝑅 𝐵
2		3brtr3.2	⊢ 𝐴 = 𝐶
3		3brtr3.3	⊢ 𝐵 = 𝐷
4	2 1	eqbrtrri	⊢ 𝐶 𝑅 𝐵
5	4 3	breqtri	⊢ 𝐶 𝑅 𝐷