Theorem ineqan12d 4174

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3911

This theorem is referenced by:  funprg  6575  funtpg  6576  funcnvpr  6583  funcnvqp  6585  fvun1  6958  fndmin  7026  ofrfvalg  7668  offval  7669  offval3  7963  fpar  8095  offsplitfpar  8098  fisn  9373  ixxin  13366  vdwmc  17014  fvcosymgeq  19469  cssincl  21740  inmbl  25604  iundisj2  25611  itg1addlem3  25760  fh1  31821  iundisj2f  32790  of0r  32881  iundisj2fi  32999  satffunlem1lem1  35752  satffunlem2lem1  35754  disjeccnvep  38789  disjecxrn  38911  br1cosscnvxrn  39063