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 ⊢ A = B
eqbrtr.2 ⊢ B R C
Assertion eqbrtri ⊢ A R C

Proof

Step Hyp Ref Expression
1 eqbrtr.1 ⊢ A = B
2 eqbrtr.2 ⊢ B R C
3 1 breq1i ⊢ A R C ↔ B R C
4 2 3 mpbir ⊢ A R C