Metamath Proof Explorer


Theorem breqtrrid

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005)

Ref Expression
Hypotheses breqtrrid.1 ARB
breqtrrid.2 φC=B
Assertion breqtrrid φARC

Proof

Step Hyp Ref Expression
1 breqtrrid.1 ARB
2 breqtrrid.2 φC=B
3 2 eqcomd φB=C
4 1 3 breqtrid φARC