Theorem breqtrid

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

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

Proof

Step	Hyp	Ref	Expression
1		breqtrid.1	|- A R B
2		breqtrid.2	|- ( ph -> B = C )
3	1	a1i	|- ( ph -> A R B )
4	3 2	breqtrd	|- ( ph -> A R C )