Theorem ineq12i 4239

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

Syntax hints:   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  undir  4306  difundi  4309  difindir  4312  inrab  4335  inrab2  4336  elneldisj  4415  dfif4  4563  dfif5  4564  inxpOLD  5857  resindi  6025  resindir  6026  rnin  6178  inimass  6186  cnvrescnv  6226  predin  6359  funtp  6635  orduniss2  7869  offres  8024  fodomr  9194  fodomfir  9396  epinid0  9669  cnvepnep  9677  wemapwe  9766  cotr3  15027  explecnv  15913  psssdm2  18651  ablfacrp  20110  cnfldfunALT  21402  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  pjfval2  21752  ofco2  22478  iundisj2  25603  clwwlknondisj  30143  lejdiri  31571  cmbr3i  31632  nonbooli  31683  5oai  31693  3oalem5  31698  mayetes3i  31761  mdexchi  32367  disjpreima  32606  disjxpin  32610  iundisj2f  32612  xppreima  32664  iundisj2fi  32802  xpinpreima  33852  xpinpreima2  33853  ordtcnvNEW  33866  pprodcnveq  35847  dfiota3  35887  bj-inrab  36893  ptrest  37579  ftc1anclem6  37658  xrnres3  38360  br2coss  38394  1cosscnvxrn  38431  refsymrels2  38521  dfeqvrels2  38544  dfeldisj5  38677  dnwech  43005  fgraphopab  43164  onfrALTlem5  44513  onfrALTlem4  44514  onfrALTlem5VD  44856  onfrALTlem4VD  44857  disjxp1  44971  disjinfi  45099