Theorem ineqan12d 4170

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∩ cin 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-in 3907

This theorem is referenced by:  funprg  6531  funtpg  6532  funcnvpr  6539  funcnvqp  6541  fvun1  6908  fndmin  6973  ofrfvalg  7613  offval  7614  offval3  7909  fpar  8041  offsplitfpar  8044  fisn  9306  ixxin  13254  vdwmc  16882  fvcosymgeq  19334  cssincl  21618  inmbl  25463  iundisj2  25470  itg1addlem3  25619  fh1  31588  iundisj2f  32560  of0r  32650  iundisj2fi  32769  satffunlem1lem1  35414  satffunlem2lem1  35416  disjeccnvep  38297  disjecxrn  38400  br1cosscnvxrn  38490