Theorem ineq12i 4185

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

Syntax hints:   = wceq 1531   ∩ cin 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1534  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-rab 3145  df-in 3941

This theorem is referenced by:  undir  4251  difundi  4254  difindir  4257  inrab  4273  inrab2  4274  elneldisj  4340  dfif4  4480  dfif5  4481  inxp  5696  resindi  5862  resindir  5863  rnin  5998  inimass  6005  cnvrescnv  6045  predin  6164  funtp  6404  orduniss2  7540  offres  7676  fodomr  8660  epinid0  9056  cnvepnep  9063  wemapwe  9152  cotr3  14330  explecnv  15212  psssdm2  17817  ablfacrp  19180  cnfldfun  20549  pjfval2  20845  ofco2  21052  iundisj2  24142  clwwlknondisj  27882  lejdiri  29308  cmbr3i  29369  nonbooli  29420  5oai  29430  3oalem5  29435  mayetes3i  29498  mdexchi  30104  disjpreima  30326  disjxpin  30330  iundisj2f  30332  xppreima  30386  iundisj2fi  30512  xpinpreima  31142  xpinpreima2  31143  ordtcnvNEW  31156  pprodcnveq  33337  dfiota3  33377  bj-inrab  34238  ptrest  34883  ftc1anclem6  34964  xrnres3  35644  br2coss  35675  1cosscnvxrn  35707  refsymrels2  35793  dfeqvrels2  35815  dfeldisj5  35946  dnwech  39638  fgraphopab  39800  onfrALTlem5  40866  onfrALTlem4  40867  onfrALTlem5VD  41209  onfrALTlem4VD  41210  disjxp1  41321  disjinfi  41443