Theorem ineq12i 4210

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 4207	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	mp2an 690	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

Syntax hints:   = wceq 1541   ∩ cin 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955

This theorem is referenced by:  undir  4276  difundi  4279  difindir  4282  inrab  4306  inrab2  4307  elneldisj  4388  dfif4  4543  dfif5  4544  inxp  5832  resindi  5997  resindir  5998  rnin  6146  inimass  6154  cnvrescnv  6194  predin  6328  funtp  6605  orduniss2  7823  offres  7972  fodomr  9130  epinid0  9597  cnvepnep  9605  wemapwe  9694  cotr3  14929  explecnv  15815  psssdm2  18538  ablfacrp  19977  cnfldfunALT  21157  cnfldfunALTOLD  21158  pjfval2  21483  ofco2  22173  iundisj2  25290  clwwlknondisj  29619  lejdiri  31047  cmbr3i  31108  nonbooli  31159  5oai  31169  3oalem5  31174  mayetes3i  31237  mdexchi  31843  disjpreima  32070  disjxpin  32074  iundisj2f  32076  xppreima  32126  iundisj2fi  32263  xpinpreima  33172  xpinpreima2  33173  ordtcnvNEW  33186  pprodcnveq  35147  dfiota3  35187  gg-cnfldfunALT  35484  bj-inrab  36110  ptrest  36790  ftc1anclem6  36869  xrnres3  37577  br2coss  37611  1cosscnvxrn  37648  refsymrels2  37738  dfeqvrels2  37761  dfeldisj5  37894  dnwech  42092  fgraphopab  42254  onfrALTlem5  43605  onfrALTlem4  43606  onfrALTlem5VD  43948  onfrALTlem4VD  43949  disjxp1  44058  disjinfi  44190