Theorem breqtrri

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999)

	Ref	Expression
Hypotheses	breqtrr.1	$$⊢ARB$$
	breqtrr.2	$$⊢C=B$$
Assertion	breqtrri	$$⊢ARC$$

Proof

Step	Hyp	Ref	Expression
1		breqtrr.1	$$⊢ARB$$
2		breqtrr.2	$$⊢C=B$$
3	2	eqcomi	$$⊢B=C$$
4	1 3	breqtri	$$⊢ARC$$