Theorem breqtri

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

	Ref	Expression
Hypotheses	breqtr.1	|- A R B
	breqtr.2	|- B = C
Assertion	breqtri	|- A R C

Proof

Step	Hyp	Ref	Expression
1		breqtr.1	|- A R B
2		breqtr.2	|- B = C
3	2	breq2i	|- ( A R B <-> A R C )
4	1 3	mpbi	|- A R C