Theorem ineqan12d 4175

Description: Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)

Hypotheses

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
ineqan12d.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
ineqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Proof of Theorem ineqan12d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineqan12d.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		ineq12 4168	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	syl2an 608	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  funprg  6594  funtpg  6595  funcnvpr  6602  funcnvqp  6604  fvun1  6976  fndmin  7044  ofrfvalg  7692  offval  7693  offval3  7985  fpar  8117  offsplitfpar  8120  fisn  9394  ixxin  13409  vdwmc  17064  fvcosymgeq  19547  cssincl  21892  inmbl  25756  iundisj2  25763  itg1addlem3  25912  fh1  32045  iundisj2f  33010  of0r  33099  iundisj2fi  33216  satffunlem1lem1  35935  satffunlem2lem1  35937  disjeccnvep  39001  disjecxrn  39123  br1cosscnvxrn  39275