This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqbrtri

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999)

Ref Expression
Hypotheses eqbrtr.1 ⊢ 𝐴 = 𝐵
eqbrtr.2 ⊢ 𝐵 𝑅 𝐶
Assertion eqbrtri 𝐴 𝑅 𝐶

Proof

Step Hyp Ref Expression
1 eqbrtr.1 ⊢ 𝐴 = 𝐵
2 eqbrtr.2 ⊢ 𝐵 𝑅 𝐶
3 1 breq1i ⊢ ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 )
4 2 3 mpbir ⊢ 𝐴 𝑅 𝐶