Theorem ineq12i 4165

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

Syntax hints:   = wceq 1541   ∩ cin 3896

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904

This theorem is referenced by:  undir  4234  difundi  4237  difindir  4240  inrab  4263  inrab2  4264  elneldisj  4339  dfif4  4488  dfif5  4489  inxpOLD  5771  resindi  5943  resindir  5944  rnin  6093  inimass  6102  cnvrescnv  6142  predin  6274  funtp  6538  orduniss2  7763  offres  7915  fodomr  9041  fodomfir  9212  epinid0  9489  cnvepnep  9498  wemapwe  9587  cotr3  14885  explecnv  15772  psssdm2  18487  ablfacrp  19980  cnfldfunALT  21306  cnfldfunALTOLD  21319  pjfval2  21646  ofco2  22366  iundisj2  25477  clwwlknondisj  30091  lejdiri  31519  cmbr3i  31580  nonbooli  31631  5oai  31641  3oalem5  31646  mayetes3i  31709  mdexchi  32315  disjpreima  32564  disjxpin  32568  iundisj2f  32570  xppreima  32627  iundisj2fi  32779  xpinpreima  33919  xpinpreima2  33920  ordtcnvNEW  33933  pprodcnveq  35925  dfiota3  35965  bj-inrab  36971  ptrest  37669  ftc1anclem6  37748  dmxrn  38421  xrnres3  38461  br2coss  38550  1cosscnvxrn  38587  refsymrels2  38671  dfeqvrels2  38694  dfeldisj5  38829  dnwech  43151  fgraphopab  43306  onfrALTlem5  44645  onfrALTlem4  44646  onfrALTlem5VD  44987  onfrALTlem4VD  44988  disjxp1  45176  disjinfi  45299  oppczeroo  49348