Theorem ineq12i 4171

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

Syntax hints:   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  undir  4240  difundi  4243  difindir  4246  inrab  4269  inrab2  4270  elneldisj  4349  dfif4  4503  dfif5  4504  resindi  5994  resindir  5995  rninOLD  6144  inimass  6152  cnvrescnv  6194  predin  6328  funtp  6593  orduniss2  7825  offres  7976  fodomr  9112  fodomfir  9283  epinid0  9563  cnvepnep  9573  wemapwe  9662  cotr3  15011  explecnv  15915  psssdm2  18632  ablfacrp  20133  cnfldfunALT  21537  pjfval2  21859  ofco2  22608  iundisj2  25708  clwwlknondisj  30462  lejdiri  31891  cmbr3i  31952  nonbooli  32003  5oai  32013  3oalem5  32018  mayetes3i  32081  mdexchi  32687  disjpreima  32929  disjxpin  32933  iundisj2f  32935  xppreima  32990  iundisj2fi  33142  xpinpreima  34296  xpinpreima2  34297  ordtcnvNEW  34310  pprodcnveq  36373  dfiota3  36413  bj-inrab  37583  ptrest  38290  ftc1anclem6  38369  dmxrn  39056  xrnres3  39096  br2coss  39197  1cosscnvxrn  39234  refsymrels2  39318  dfeqvrels2  39341  dfeldisj5  39482  dnwech  43795  fgraphopab  43950  onfrALTlem5  45271  onfrALTlem4  45272  onfrALTlem5VD  45613  onfrALTlem4VD  45614  disjxp1  45809  disjinfi  45930  oppczeroo  50035