Theorem ineq12i 4181

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

Syntax hints:   = wceq 1540   ∩ cin 3913

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 3406  df-in 3921

This theorem is referenced by:  undir  4250  difundi  4253  difindir  4256  inrab  4279  inrab2  4280  elneldisj  4355  dfif4  4504  dfif5  4505  inxpOLD  5796  resindi  5966  resindir  5967  rnin  6119  inimass  6128  cnvrescnv  6168  predin  6300  funtp  6573  orduniss2  7808  offres  7962  fodomr  9092  fodomfir  9279  epinid0  9553  cnvepnep  9561  wemapwe  9650  cotr3  14944  explecnv  15831  psssdm2  18540  ablfacrp  19998  cnfldfunALT  21279  cnfldfunALTOLD  21292  pjfval2  21618  ofco2  22338  iundisj2  25450  clwwlknondisj  30040  lejdiri  31468  cmbr3i  31529  nonbooli  31580  5oai  31590  3oalem5  31595  mayetes3i  31658  mdexchi  32264  disjpreima  32513  disjxpin  32517  iundisj2f  32519  xppreima  32569  iundisj2fi  32720  xpinpreima  33896  xpinpreima2  33897  ordtcnvNEW  33910  pprodcnveq  35871  dfiota3  35911  bj-inrab  36915  ptrest  37613  ftc1anclem6  37692  dmxrn  38360  xrnres3  38390  br2coss  38429  1cosscnvxrn  38466  refsymrels2  38556  dfeqvrels2  38579  dfeldisj5  38713  dnwech  43037  fgraphopab  43192  onfrALTlem5  44532  onfrALTlem4  44533  onfrALTlem5VD  44874  onfrALTlem4VD  44875  disjxp1  45063  disjinfi  45186  oppczeroo  49223