Theorem breqtrid

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

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

Proof

Step	Hyp	Ref	Expression
1		breqtrid.1	$$⊢ARB$$
2		breqtrid.2	$$⊢\phi \to B=C$$
3	1	a1i	$$⊢\phi \to ARB$$
4	3 2	breqtrd	$$⊢\phi \to ARC$$