Theorem breqtrri

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

	Ref	Expression
Hypotheses	breqtrr.1	|- A R B
	breqtrr.2	|- C = B
Assertion	breqtrri	|- A R C

Proof

Step	Hyp	Ref	Expression
1		breqtrr.1	|- A R B
2		breqtrr.2	|- C = B
3	2	eqcomi	|- B = C
4	1 3	breqtri	|- A R C