Theorem ineq12i 3947

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

Syntax hints:   = wceq 1624   ∩ cin 3706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-in 3714

This theorem is referenced by:  undir  4011  difundi  4014  difindir  4017  inrab  4034  inrab2  4035  elneldisj  4098  elneldisjOLD  4100  dfif4  4237  dfif5  4238  inxp  5402  resindi  5562  resindir  5563  rnin  5692  inimass  5699  predin  5856  funtp  6098  orduniss2  7190  offres  7320  fodomr  8268  epinid0  8662  cnvepnep  8668  wemapwe  8759  cotr3  13910  explecnv  14788  psssdm2  17408  ablfacrp  18657  cnfldfun  19952  pjfval2  20247  ofco2  20451  iundisj2  23509  clwwlknondisj  27252  lejdiri  28699  cmbr3i  28760  nonbooli  28811  5oai  28821  3oalem5  28826  mayetes3i  28889  mdexchi  29495  disjpreima  29696  disjxpin  29700  iundisj2f  29702  xppreima  29750  iundisj2fi  29857  xpinpreima  30253  xpinpreima2  30254  ordtcnvNEW  30267  pprodcnveq  32288  dfiota3  32328  bj-inrab  33221  ptrest  33713  ftc1anclem6  33795  xrnres3  34477  br2coss  34508  1cosscnvxrn  34540  refsymrels2  34626  dnwech  38112  fgraphopab  38282  onfrALTlem5  39251  onfrALTlem4  39252  onfrALTlem5VD  39612  onfrALTlem4VD  39613  disjxp1  39729  disjinfi  39871