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 692	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)

Syntax hints:   = wceq 1541   ∩ cin 3900

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  undir  4239  difundi  4242  difindir  4245  inrab  4268  inrab2  4269  elneldisj  4344  dfif4  4495  dfif5  4496  inxpOLD  5781  resindi  5954  resindir  5955  rnin  6104  inimass  6113  cnvrescnv  6153  predin  6285  funtp  6549  orduniss2  7775  offres  7927  fodomr  9056  fodomfir  9228  epinid0  9508  cnvepnep  9517  wemapwe  9606  cotr3  14901  explecnv  15788  psssdm2  18504  ablfacrp  19997  cnfldfunALT  21324  cnfldfunALTOLD  21337  pjfval2  21664  ofco2  22395  iundisj2  25506  clwwlknondisj  30186  lejdiri  31614  cmbr3i  31675  nonbooli  31726  5oai  31736  3oalem5  31741  mayetes3i  31804  mdexchi  32410  disjpreima  32659  disjxpin  32663  iundisj2f  32665  xppreima  32723  iundisj2fi  32877  xpinpreima  34063  xpinpreima2  34064  ordtcnvNEW  34077  pprodcnveq  36075  dfiota3  36115  bj-inrab  37128  ptrest  37820  ftc1anclem6  37899  dmxrn  38582  xrnres3  38622  br2coss  38711  1cosscnvxrn  38748  refsymrels2  38832  dfeqvrels2  38855  dfeldisj5  38990  dnwech  43300  fgraphopab  43455  onfrALTlem5  44793  onfrALTlem4  44794  onfrALTlem5VD  45135  onfrALTlem4VD  45136  disjxp1  45324  disjinfi  45446  oppczeroo  49492