Metamath Proof Explorer


Theorem eqbrtrrid

Description: A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004)

Ref Expression
Hypotheses eqbrtrrid.1
|- B = A
eqbrtrrid.2
|- ( ph -> B R C )
Assertion eqbrtrrid
|- ( ph -> A R C )

Proof

Step Hyp Ref Expression
1 eqbrtrrid.1
 |-  B = A
2 eqbrtrrid.2
 |-  ( ph -> B R C )
3 eqid
 |-  C = C
4 2 1 3 3brtr3g
 |-  ( ph -> A R C )