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


Ref 
Expression 

Hypotheses 
3eqtr4i.1 
⊢ 𝐴 = 𝐵 


3eqtr4i.2 
⊢ 𝐶 = 𝐴 


3eqtr4i.3 
⊢ 𝐷 = 𝐵 

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

3eqtr4i.1 
⊢ 𝐴 = 𝐵 
2 

3eqtr4i.2 
⊢ 𝐶 = 𝐴 
3 

3eqtr4i.3 
⊢ 𝐷 = 𝐵 
4 
3 1

eqtr4i 
⊢ 𝐷 = 𝐴 
5 
2 4

eqtr4i 
⊢ 𝐶 = 𝐷 