Theorem ineqan12d 4141

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888

This theorem is referenced by:  funprg  6378  funtpg  6379  funcnvpr  6386  funcnvqp  6388  fvun1  6729  fndmin  6792  offval  7396  ofrfval  7397  offval3  7665  fpar  7794  offsplitfpar  7798  wfrlem4  7941  fisn  8875  ixxin  12743  vdwmc  16304  fvcosymgeq  18549  cssincl  20377  inmbl  24146  iundisj2  24153  itg1addlem3  24302  fh1  29401  iundisj2f  30353  iundisj2fi  30546  satffunlem1lem1  32762  satffunlem2lem1  32764  br1cosscnvxrn  35874