Theorem ineq12i 4170

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

Syntax hints:   = 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:  undir  4239  difundi  4242  difindir  4245  inrab  4268  inrab2  4269  elneldisj  4346  dfif4  4496  dfif5  4497  resindi  5981  resindir  5982  rninOLD  6131  inimass  6140  cnvrescnv  6182  predin  6314  funtp  6578  orduniss2  7813  offres  7964  fodomr  9100  fodomfir  9272  epinid0  9553  cnvepnep  9563  wemapwe  9652  cotr3  14991  explecnv  15895  psssdm2  18613  ablfacrp  20108  cnfldfunALT  21439  pjfval2  21761  ofco2  22511  iundisj2  25611  clwwlknondisj  30313  lejdiri  31742  cmbr3i  31803  nonbooli  31854  5oai  31864  3oalem5  31869  mayetes3i  31932  mdexchi  32538  disjpreima  32784  disjxpin  32788  iundisj2f  32790  xppreima  32847  iundisj2fi  32999  xpinpreima  34203  xpinpreima2  34204  ordtcnvNEW  34217  pprodcnveq  36231  dfiota3  36271  bj-inrab  37412  ptrest  38118  ftc1anclem6  38197  dmxrn  38886  xrnres3  38926  br2coss  39027  1cosscnvxrn  39064  refsymrels2  39148  dfeqvrels2  39171  dfeldisj5  39312  dnwech  43625  fgraphopab  43780  onfrALTlem5  45118  onfrALTlem4  45119  onfrALTlem5VD  45460  onfrALTlem4VD  45461  disjxp1  45649  disjinfi  45770  oppczeroo  49858