Theorem ineq12i 4144

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

Syntax hints:   = wceq 1539   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-in 3894

This theorem is referenced by:  undir  4210  difundi  4213  difindir  4216  inrab  4240  inrab2  4241  elneldisj  4322  dfif4  4474  dfif5  4475  inxp  5741  resindi  5907  resindir  5908  rnin  6050  inimass  6058  cnvrescnv  6098  predin  6230  funtp  6491  orduniss2  7680  offres  7826  fodomr  8915  epinid0  9359  cnvepnep  9366  wemapwe  9455  cotr3  14689  explecnv  15577  psssdm2  18299  ablfacrp  19669  cnfldfunALT  20610  cnfldfunALTOLD  20611  pjfval2  20916  ofco2  21600  iundisj2  24713  clwwlknondisj  28475  lejdiri  29901  cmbr3i  29962  nonbooli  30013  5oai  30023  3oalem5  30028  mayetes3i  30091  mdexchi  30697  disjpreima  30923  disjxpin  30927  iundisj2f  30929  xppreima  30983  iundisj2fi  31118  xpinpreima  31856  xpinpreima2  31857  ordtcnvNEW  31870  pprodcnveq  34185  dfiota3  34225  bj-inrab  35115  ptrest  35776  ftc1anclem6  35855  xrnres3  36530  br2coss  36561  1cosscnvxrn  36593  refsymrels2  36679  dfeqvrels2  36701  dfeldisj5  36832  dnwech  40873  fgraphopab  41035  onfrALTlem5  42162  onfrALTlem4  42163  onfrALTlem5VD  42505  onfrALTlem4VD  42506  disjxp1  42617  disjinfi  42731