Metamath Proof Explorer
Description: A deduction from three chained equalities. (Contributed by NM, 21Sep1995)


Ref 
Expression 

Hypotheses 
3eqtr4d.1 
 ( ph > A = B ) 


3eqtr4d.2 
 ( ph > C = A ) 


3eqtr4d.3 
 ( ph > D = B ) 

Assertion 
3eqtr4rd 
 ( ph > D = C ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3eqtr4d.1 
 ( ph > A = B ) 
2 

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

3eqtr4d.3 
 ( ph > D = B ) 
4 
3 1

eqtr4d 
 ( ph > D = A ) 
5 
4 2

eqtr4d 
 ( ph > D = C ) 