Metamath Proof Explorer
Description: An inference from three chained equalities. (Contributed by NM, 2Sep1995) (Proof shortened by Andrew Salmon, 25May2011)


Ref 
Expression 

Hypotheses 
3eqtr4i.1 
⊢ 𝐴 = 𝐵 


3eqtr4i.2 
⊢ 𝐶 = 𝐴 


3eqtr4i.3 
⊢ 𝐷 = 𝐵 

Assertion 
3eqtr4ri 
⊢ 𝐷 = 𝐶 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3eqtr4i.1 
⊢ 𝐴 = 𝐵 
2 

3eqtr4i.2 
⊢ 𝐶 = 𝐴 
3 

3eqtr4i.3 
⊢ 𝐷 = 𝐵 
4 
3 1

eqtr4i 
⊢ 𝐷 = 𝐴 
5 
4 2

eqtr4i 
⊢ 𝐷 = 𝐶 