Theorem ineq12i 3774

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

Syntax hints:   = wceq 1475   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  undir  3835  difundi  3838  difindir  3841  inrab  3858  inrab2  3859  elneldisj  3917  dfif4  4051  dfif5  4052  inxp  5176  resindi  5332  resindir  5333  rnin  5461  inimass  5468  predin  5620  funtp  5859  orduniss2  6925  offres  7054  fodomr  7996  wemapwe  8477  cotr3  13565  explecnv  14436  psssdm2  17038  ablfacrp  18288  pjfval2  19872  ofco2  20076  iundisj2  23124  lejdiri  27782  cmbr3i  27843  nonbooli  27894  5oai  27904  3oalem5  27909  mayetes3i  27972  mdexchi  28578  disjpreima  28779  disjxpin  28783  iundisj2f  28785  xppreima  28829  iundisj2fi  28943  xpinpreima  29280  xpinpreima2  29281  ordtcnvNEW  29294  pprodcnveq  31160  dfiota3  31200  bj-inrab  32115  ptrest  32578  ftc1anclem6  32660  dnwech  36636  fgraphopab  36807  onfrALTlem5  37778  onfrALTlem4  37779  onfrALTlem5VD  38143  onfrALTlem4VD  38144  disjxp1  38263  disjinfi  38375