Theorem 3brtr3i

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

	Ref	Expression
Hypotheses	3brtr3.1	$$⊢ARB$$
	3brtr3.2	$$⊢A=C$$
	3brtr3.3	$$⊢B=D$$
Assertion	3brtr3i	$$⊢CRD$$

Proof

Step	Hyp	Ref	Expression
1		3brtr3.1	$$⊢ARB$$
2		3brtr3.2	$$⊢A=C$$
3		3brtr3.3	$$⊢B=D$$
4	2 1	eqbrtrri	$$⊢CRB$$
5	4 3	breqtri	$$⊢CRD$$