Theorem ineq12i 4177

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

Syntax hints:   = wceq 1540   ∩ cin 3910

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  undir  4246  difundi  4249  difindir  4252  inrab  4275  inrab2  4276  elneldisj  4351  dfif4  4500  dfif5  4501  inxpOLD  5786  resindi  5955  resindir  5956  rnin  6107  inimass  6116  cnvrescnv  6156  predin  6288  funtp  6557  orduniss2  7788  offres  7941  fodomr  9069  fodomfir  9255  epinid0  9529  cnvepnep  9537  wemapwe  9626  cotr3  14920  explecnv  15807  psssdm2  18522  ablfacrp  19982  cnfldfunALT  21311  cnfldfunALTOLD  21324  pjfval2  21651  ofco2  22371  iundisj2  25483  clwwlknondisj  30090  lejdiri  31518  cmbr3i  31579  nonbooli  31630  5oai  31640  3oalem5  31645  mayetes3i  31708  mdexchi  32314  disjpreima  32563  disjxpin  32567  iundisj2f  32569  xppreima  32619  iundisj2fi  32770  xpinpreima  33889  xpinpreima2  33890  ordtcnvNEW  33903  pprodcnveq  35864  dfiota3  35904  bj-inrab  36908  ptrest  37606  ftc1anclem6  37685  dmxrn  38353  xrnres3  38383  br2coss  38422  1cosscnvxrn  38459  refsymrels2  38549  dfeqvrels2  38572  dfeldisj5  38706  dnwech  43030  fgraphopab  43185  onfrALTlem5  44525  onfrALTlem4  44526  onfrALTlem5VD  44867  onfrALTlem4VD  44868  disjxp1  45056  disjinfi  45179  oppczeroo  49219