Metamath Proof Explorer
Description: An equality transitivity equality deduction. (Contributed by NM, 18Jul1995)


Ref 
Expression 

Hypotheses 
eqtr4d.1 
 ( ph > A = B ) 


eqtr4d.2 
 ( ph > C = B ) 

Assertion 
eqtr4d 
 ( ph > A = C ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqtr4d.1 
 ( ph > A = B ) 
2 

eqtr4d.2 
 ( ph > C = B ) 
3 
2

eqcomd 
 ( ph > B = C ) 
4 
1 3

eqtrd 
 ( ph > A = C ) 