Theorem ineq12i 4190

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

Syntax hints:   = wceq 1536   ∩ cin 3938

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1539  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3150  df-in 3946

This theorem is referenced by:  undir  4256  difundi  4259  difindir  4262  inrab  4278  inrab2  4279  elneldisj  4345  dfif4  4485  dfif5  4486  inxp  5706  resindi  5872  resindir  5873  rnin  6008  inimass  6015  cnvrescnv  6055  predin  6174  funtp  6414  orduniss2  7551  offres  7687  fodomr  8671  epinid0  9067  cnvepnep  9074  wemapwe  9163  cotr3  14341  explecnv  15223  psssdm2  17828  ablfacrp  19191  cnfldfun  20560  pjfval2  20856  ofco2  21063  iundisj2  24153  clwwlknondisj  27893  lejdiri  29319  cmbr3i  29380  nonbooli  29431  5oai  29441  3oalem5  29446  mayetes3i  29509  mdexchi  30115  disjpreima  30337  disjxpin  30341  iundisj2f  30343  xppreima  30397  iundisj2fi  30523  xpinpreima  31153  xpinpreima2  31154  ordtcnvNEW  31167  pprodcnveq  33348  dfiota3  33388  bj-inrab  34249  ptrest  34895  ftc1anclem6  34976  xrnres3  35656  br2coss  35687  1cosscnvxrn  35719  refsymrels2  35805  dfeqvrels2  35827  dfeldisj5  35958  dnwech  39654  fgraphopab  39816  onfrALTlem5  40882  onfrALTlem4  40883  onfrALTlem5VD  41225  onfrALTlem4VD  41226  disjxp1  41337  disjinfi  41460