Metamath Proof Explorer
Description: A chained equality inference for a binary relation. (Contributed by NM, 24Apr2005)


Ref 
Expression 

Hypotheses 
breqtrrdi.1 
 ( ph > A R B ) 


breqtrrdi.2 
 C = B 

Assertion 
breqtrrdi 
 ( ph > A R C ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

breqtrrdi.1 
 ( ph > A R B ) 
2 

breqtrrdi.2 
 C = B 
3 
2

eqcomi 
 B = C 
4 
1 3

breqtrdi 
 ( ph > A R C ) 