Metamath Proof Explorer
Description: A deduction from three chained equalities. (Contributed by NM, 4Aug2006) (Proof shortened by Andrew Salmon, 25May2011)


Ref 
Expression 

Hypotheses 
3eqtrd.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 


3eqtrd.2 
⊢ ( 𝜑 → 𝐵 = 𝐶 ) 


3eqtrd.3 
⊢ ( 𝜑 → 𝐶 = 𝐷 ) 

Assertion 
3eqtrrd 
⊢ ( 𝜑 → 𝐷 = 𝐴 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3eqtrd.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 
2 

3eqtrd.2 
⊢ ( 𝜑 → 𝐵 = 𝐶 ) 
3 

3eqtrd.3 
⊢ ( 𝜑 → 𝐶 = 𝐷 ) 
4 
1 2

eqtrd 
⊢ ( 𝜑 → 𝐴 = 𝐶 ) 
5 
4 3

eqtr2d 
⊢ ( 𝜑 → 𝐷 = 𝐴 ) 