Theorem breqtrid

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

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

Proof

Step	Hyp	Ref	Expression
1		breqtrid.1	⊢ 𝐴 𝑅 𝐵
2		breqtrid.2	⊢ ( 𝜑 → 𝐵 = 𝐶 )
3	1	a1i	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
4	3 2	breqtrd	⊢ ( 𝜑 → 𝐴 𝑅 𝐶 )