Metamath Proof Explorer
Description: A chained equality inference, useful for converting from definitions.
(Contributed by NM, 15Nov1994)


Ref 
Expression 

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


3eqtr3g.2 
 A = C 


3eqtr3g.3 
 B = D 

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

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

3eqtr3g.2 
 A = C 
3 

3eqtr3g.3 
 B = D 
4 
2 1

syl5eqr 
 ( ph > C = B ) 
5 
4 3

eqtrdi 
 ( ph > C = D ) 