Metamath Proof Explorer
Description: Equality deduction for operation value. (Contributed by NM, 10Aug1995)


Ref 
Expression 

Hypotheses 
oveq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 


opreqan12i.2 
⊢ ( 𝜓 → 𝐶 = 𝐷 ) 

Assertion 
oveqan12d 
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 𝐹 𝐶 ) = ( 𝐵 𝐹 𝐷 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

oveq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 
2 

opreqan12i.2 
⊢ ( 𝜓 → 𝐶 = 𝐷 ) 
3 

oveq12 
⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( 𝐴 𝐹 𝐶 ) = ( 𝐵 𝐹 𝐷 ) ) 
4 
1 2 3

syl2an 
⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 𝐹 𝐶 ) = ( 𝐵 𝐹 𝐷 ) ) 