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


Ref 
Expression 

Hypotheses 
breqtrid.1 
 A R B 


breqtrid.2 
 ( ph > B = C ) 

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

breqtrid.1 
 A R B 
2 

breqtrid.2 
 ( ph > B = C ) 
3 
1

a1i 
 ( ph > A R B ) 
4 
3 2

breqtrd 
 ( ph > A R C ) 