Metamath Proof Explorer
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10Apr1994)


Ref 
Expression 

Hypothesis 
ineq1d.1 
⊢ ( 𝜑 → 𝐴 = 𝐵 ) 

Assertion 
ineq1d 
⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

ineq1 
⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) 
3 
1 2

syl 
⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) 