Theorem ineq12i 4172

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

Syntax hints:   = wceq 1542   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910

This theorem is referenced by:  undir  4241  difundi  4244  difindir  4247  inrab  4270  inrab2  4271  elneldisj  4346  dfif4  4497  dfif5  4498  inxpOLD  5789  resindi  5962  resindir  5963  rnin  6112  inimass  6121  cnvrescnv  6161  predin  6293  funtp  6557  orduniss2  7785  offres  7937  fodomr  9068  fodomfir  9240  epinid0  9520  cnvepnep  9529  wemapwe  9618  cotr3  14913  explecnv  15800  psssdm2  18516  ablfacrp  20009  cnfldfunALT  21336  cnfldfunALTOLD  21349  pjfval2  21676  ofco2  22407  iundisj2  25518  clwwlknondisj  30198  lejdiri  31627  cmbr3i  31688  nonbooli  31739  5oai  31749  3oalem5  31754  mayetes3i  31817  mdexchi  32423  disjpreima  32671  disjxpin  32675  iundisj2f  32677  xppreima  32735  iundisj2fi  32888  xpinpreima  34084  xpinpreima2  34085  ordtcnvNEW  34098  pprodcnveq  36097  dfiota3  36137  bj-inrab  37175  ptrest  37870  ftc1anclem6  37949  dmxrn  38638  xrnres3  38678  br2coss  38779  1cosscnvxrn  38816  refsymrels2  38900  dfeqvrels2  38923  dfeldisj5  39064  dnwech  43405  fgraphopab  43560  onfrALTlem5  44898  onfrALTlem4  44899  onfrALTlem5VD  45240  onfrALTlem4VD  45241  disjxp1  45429  disjinfi  45551  oppczeroo  49596