Theorem eqbrtrrdi

Description: A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006)

	Ref	Expression
Hypotheses	eqbrtrrdi.1	$$⊢\phi \to B=A$$
	eqbrtrrdi.2	$$⊢BRC$$
Assertion	eqbrtrrdi	$$⊢\phi \to ARC$$

Proof

Step	Hyp	Ref	Expression
1		eqbrtrrdi.1	$$⊢\phi \to B=A$$
2		eqbrtrrdi.2	$$⊢BRC$$
3	1	eqcomd	$$⊢\phi \to A=B$$
4	3 2	eqbrtrdi	$$⊢\phi \to ARC$$