Theorem breqtrdi

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

	Ref	Expression
Hypotheses	breqtrdi.1	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
	breqtrdi.2	⊢ 𝐵 = 𝐶
Assertion	breqtrdi	⊢ ( 𝜑 → 𝐴 𝑅 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		breqtrdi.1	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
2		breqtrdi.2	⊢ 𝐵 = 𝐶
3		eqid	⊢ 𝐴 = 𝐴
4	1 3 2	3brtr3g	⊢ ( 𝜑 → 𝐴 𝑅 𝐶 )