Theorem ineq12i 4169

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

Syntax hints:   = wceq 1540   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910

This theorem is referenced by:  undir  4238  difundi  4241  difindir  4244  inrab  4267  inrab2  4268  elneldisj  4343  dfif4  4492  dfif5  4493  inxpOLD  5775  resindi  5946  resindir  5947  rnin  6095  inimass  6104  cnvrescnv  6144  predin  6275  funtp  6539  orduniss2  7766  offres  7918  fodomr  9045  fodomfir  9218  epinid0  9495  cnvepnep  9504  wemapwe  9593  cotr3  14885  explecnv  15772  psssdm2  18487  ablfacrp  19947  cnfldfunALT  21276  cnfldfunALTOLD  21289  pjfval2  21616  ofco2  22336  iundisj2  25448  clwwlknondisj  30055  lejdiri  31483  cmbr3i  31544  nonbooli  31595  5oai  31605  3oalem5  31610  mayetes3i  31673  mdexchi  32279  disjpreima  32528  disjxpin  32532  iundisj2f  32534  xppreima  32588  iundisj2fi  32740  xpinpreima  33873  xpinpreima2  33874  ordtcnvNEW  33887  pprodcnveq  35861  dfiota3  35901  bj-inrab  36905  ptrest  37603  ftc1anclem6  37682  dmxrn  38350  xrnres3  38380  br2coss  38419  1cosscnvxrn  38456  refsymrels2  38546  dfeqvrels2  38569  dfeldisj5  38703  dnwech  43025  fgraphopab  43180  onfrALTlem5  44520  onfrALTlem4  44521  onfrALTlem5VD  44862  onfrALTlem4VD  44863  disjxp1  45051  disjinfi  45174  oppczeroo  49226