Theorem breqtrrdi

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005)

	Ref	Expression
Hypotheses	breqtrrdi.1	$$⊢\phi \to ARB$$
	breqtrrdi.2	$$⊢C=B$$
Assertion	breqtrrdi	$$⊢\phi \to ARC$$

Proof

Step	Hyp	Ref	Expression
1		breqtrrdi.1	$$⊢\phi \to ARB$$
2		breqtrrdi.2	$$⊢C=B$$
3	2	eqcomi	$$⊢B=C$$
4	1 3	breqtrdi	$$⊢\phi \to ARC$$