Theorem ineq12i 3795

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

Syntax hints:   = wceq 1480   ∩ cin 3559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-in 3567

This theorem is referenced by:  undir  3857  difundi  3860  difindir  3863  inrab  3880  inrab2  3881  elneldisj  3942  dfif4  4078  dfif5  4079  inxp  5219  resindi  5375  resindir  5376  rnin  5505  inimass  5512  predin  5665  funtp  5905  orduniss2  6981  offres  7111  fodomr  8056  wemapwe  8539  cotr3  13646  explecnv  14517  psssdm2  17131  ablfacrp  18381  cnfldfun  19672  pjfval2  19967  ofco2  20171  iundisj2  23219  lejdiri  28238  cmbr3i  28299  nonbooli  28350  5oai  28360  3oalem5  28365  mayetes3i  28428  mdexchi  29034  disjpreima  29233  disjxpin  29237  iundisj2f  29239  xppreima  29282  iundisj2fi  29389  xpinpreima  29726  xpinpreima2  29727  ordtcnvNEW  29740  pprodcnveq  31624  dfiota3  31664  bj-inrab  32562  ptrest  33026  ftc1anclem6  33108  dnwech  37084  fgraphopab  37255  onfrALTlem5  38225  onfrALTlem4  38226  onfrALTlem5VD  38590  onfrALTlem4VD  38591  disjxp1  38709  disjinfi  38840