Theorem ineq12i 4125

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

Syntax hints:   = wceq 1543   ∩ cin 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-in 3873

This theorem is referenced by:  undir  4191  difundi  4194  difindir  4197  inrab  4221  inrab2  4222  elneldisj  4303  dfif4  4454  dfif5  4455  inxp  5701  resindi  5867  resindir  5868  rnin  6010  inimass  6018  cnvrescnv  6058  predin  6185  funtp  6437  orduniss2  7612  offres  7756  fodomr  8797  epinid0  9216  cnvepnep  9223  wemapwe  9312  cotr3  14541  explecnv  15429  psssdm2  18087  ablfacrp  19453  cnfldfun  20375  pjfval2  20671  ofco2  21348  iundisj2  24446  clwwlknondisj  28194  lejdiri  29620  cmbr3i  29681  nonbooli  29732  5oai  29742  3oalem5  29747  mayetes3i  29810  mdexchi  30416  disjpreima  30642  disjxpin  30646  iundisj2f  30648  xppreima  30702  iundisj2fi  30838  xpinpreima  31570  xpinpreima2  31571  ordtcnvNEW  31584  pprodcnveq  33922  dfiota3  33962  bj-inrab  34852  ptrest  35513  ftc1anclem6  35592  xrnres3  36267  br2coss  36298  1cosscnvxrn  36330  refsymrels2  36416  dfeqvrels2  36438  dfeldisj5  36569  dnwech  40576  fgraphopab  40738  onfrALTlem5  41835  onfrALTlem4  41836  onfrALTlem5VD  42178  onfrALTlem4VD  42179  disjxp1  42290  disjinfi  42404