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


Ref 
Expression 

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


3eqtrd.2 
 ( ph > B = C ) 


3eqtrd.3 
 ( ph > C = D ) 

Assertion 
3eqtrd 
 ( ph > A = D ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

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

3eqtrd.3 
 ( ph > C = D ) 
4 
2 3

eqtrd 
 ( ph > B = D ) 
5 
1 4

eqtrd 
 ( ph > A = D ) 