Metamath Proof Explorer
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24Oct1999)


Ref 
Expression 

Hypotheses 
breqtrrd.1 
⊢ ( 𝜑 → 𝐴 𝑅 𝐵 ) 


breqtrrd.2 
⊢ ( 𝜑 → 𝐶 = 𝐵 ) 

Assertion 
breqtrrd 
⊢ ( 𝜑 → 𝐴 𝑅 𝐶 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

breqtrrd.1 
⊢ ( 𝜑 → 𝐴 𝑅 𝐵 ) 
2 

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

eqcomd 
⊢ ( 𝜑 → 𝐵 = 𝐶 ) 
4 
1 3

breqtrd 
⊢ ( 𝜑 → 𝐴 𝑅 𝐶 ) 