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


Ref 
Expression 

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


ineqan12d.2 
⊢ ( 𝜓 → 𝐶 = 𝐷 ) 

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

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

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

ineq12 
⊢ ( ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐷 ) ) 
4 
1 2 3

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