Metamath Proof Explorer
Description: A chained equality inference, useful for converting from definitions.
(Contributed by Mario Carneiro, 6Nov2015)


Ref 
Expression 

Hypotheses 
3eqtr3a.1 
⊢ 𝐴 = 𝐵 


3eqtr3a.2 
⊢ ( 𝜑 → 𝐴 = 𝐶 ) 


3eqtr3a.3 
⊢ ( 𝜑 → 𝐵 = 𝐷 ) 

Assertion 
3eqtr3a 
⊢ ( 𝜑 → 𝐶 = 𝐷 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3eqtr3a.1 
⊢ 𝐴 = 𝐵 
2 

3eqtr3a.2 
⊢ ( 𝜑 → 𝐴 = 𝐶 ) 
3 

3eqtr3a.3 
⊢ ( 𝜑 → 𝐵 = 𝐷 ) 
4 
1 3

syl5eq 
⊢ ( 𝜑 → 𝐴 = 𝐷 ) 
5 
2 4

eqtr3d 
⊢ ( 𝜑 → 𝐶 = 𝐷 ) 