Theorem breqtrdi

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999)

	Ref	Expression
Hypotheses	breqtrdi.1	|- ( ph -> A R B )
	breqtrdi.2	|- B = C
Assertion	breqtrdi	|- ( ph -> A R C )

Proof

Step	Hyp	Ref	Expression
1		breqtrdi.1	|- ( ph -> A R B )
2		breqtrdi.2	|- B = C
3		eqid	|- A = A
4	1 3 2	3brtr3g	|- ( ph -> A R C )