Theorem ineq12i 4158

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

Syntax hints:   = wceq 1542   ∩ cin 3888

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  undir  4227  difundi  4230  difindir  4233  inrab  4256  inrab2  4257  elneldisj  4332  dfif4  4482  dfif5  4483  resindi  5960  resindir  5961  rnin  6110  inimass  6119  cnvrescnv  6159  predin  6291  funtp  6555  orduniss2  7784  offres  7936  fodomr  9066  fodomfir  9238  epinid0  9519  cnvepnep  9529  wemapwe  9618  cotr3  14940  explecnv  15830  psssdm2  18547  ablfacrp  20043  cnfldfunALT  21367  pjfval2  21689  ofco2  22416  iundisj2  25516  clwwlknondisj  30181  lejdiri  31610  cmbr3i  31671  nonbooli  31722  5oai  31732  3oalem5  31737  mayetes3i  31800  mdexchi  32406  disjpreima  32654  disjxpin  32658  iundisj2f  32660  xppreima  32718  iundisj2fi  32870  xpinpreima  34050  xpinpreima2  34051  ordtcnvNEW  34064  pprodcnveq  36063  dfiota3  36103  bj-inrab  37234  ptrest  37940  ftc1anclem6  38019  dmxrn  38708  xrnres3  38748  br2coss  38849  1cosscnvxrn  38886  refsymrels2  38970  dfeqvrels2  38993  dfeldisj5  39134  dnwech  43476  fgraphopab  43631  onfrALTlem5  44969  onfrALTlem4  44970  onfrALTlem5VD  45311  onfrALTlem4VD  45312  disjxp1  45500  disjinfi  45622  oppczeroo  49712