Theorem ineqan12d 4215

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 4208	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	syl2an 594	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-in 3954

This theorem is referenced by:  funprg  6613  funtpg  6614  funcnvpr  6621  funcnvqp  6623  fvun1  6993  fndmin  7058  ofrfvalg  7698  offval  7699  offval3  7996  fpar  8130  offsplitfpar  8133  wfrlem4OLD  8342  fisn  9470  ixxin  13395  vdwmc  16980  fvcosymgeq  19427  cssincl  21684  inmbl  25562  iundisj2  25569  itg1addlem3  25718  fh1  31551  iundisj2f  32510  of0r  32596  iundisj2fi  32699  satffunlem1lem1  35230  satffunlem2lem1  35232  disjeccnvep  37982  disjecxrn  38087  br1cosscnvxrn  38172