Theorem ineq12i 4141

Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
ineq1i.1	⊢ 𝐴 = 𝐵
ineq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
ineq12i	⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

Proof of Theorem ineq12i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		ineq12 4138	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	mp2an 688	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

Syntax hints:   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  undir  4207  difundi  4210  difindir  4213  inrab  4237  inrab2  4238  elneldisj  4319  dfif4  4471  dfif5  4472  inxp  5730  resindi  5896  resindir  5897  rnin  6039  inimass  6047  cnvrescnv  6087  predin  6219  funtp  6475  orduniss2  7655  offres  7799  fodomr  8864  epinid0  9289  cnvepnep  9296  wemapwe  9385  cotr3  14617  explecnv  15505  psssdm2  18214  ablfacrp  19584  cnfldfun  20522  pjfval2  20826  ofco2  21508  iundisj2  24618  clwwlknondisj  28376  lejdiri  29802  cmbr3i  29863  nonbooli  29914  5oai  29924  3oalem5  29929  mayetes3i  29992  mdexchi  30598  disjpreima  30824  disjxpin  30828  iundisj2f  30830  xppreima  30884  iundisj2fi  31020  xpinpreima  31758  xpinpreima2  31759  ordtcnvNEW  31772  pprodcnveq  34112  dfiota3  34152  bj-inrab  35042  ptrest  35703  ftc1anclem6  35782  xrnres3  36457  br2coss  36488  1cosscnvxrn  36520  refsymrels2  36606  dfeqvrels2  36628  dfeldisj5  36759  dnwech  40789  fgraphopab  40951  onfrALTlem5  42051  onfrALTlem4  42052  onfrALTlem5VD  42394  onfrALTlem4VD  42395  disjxp1  42506  disjinfi  42620