Theorem ineq12i 4168

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

Syntax hints:   = wceq 1541   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  undir  4237  difundi  4240  difindir  4243  inrab  4266  inrab2  4267  elneldisj  4342  dfif4  4493  dfif5  4494  inxpOLD  5779  resindi  5952  resindir  5953  rnin  6102  inimass  6111  cnvrescnv  6151  predin  6283  funtp  6547  orduniss2  7773  offres  7925  fodomr  9054  fodomfir  9226  epinid0  9506  cnvepnep  9515  wemapwe  9604  cotr3  14899  explecnv  15786  psssdm2  18502  ablfacrp  19995  cnfldfunALT  21322  cnfldfunALTOLD  21335  pjfval2  21662  ofco2  22393  iundisj2  25504  clwwlknondisj  30135  lejdiri  31563  cmbr3i  31624  nonbooli  31675  5oai  31685  3oalem5  31690  mayetes3i  31753  mdexchi  32359  disjpreima  32608  disjxpin  32612  iundisj2f  32614  xppreima  32672  iundisj2fi  32826  xpinpreima  34012  xpinpreima2  34013  ordtcnvNEW  34026  pprodcnveq  36024  dfiota3  36064  bj-inrab  37071  ptrest  37759  ftc1anclem6  37838  dmxrn  38511  xrnres3  38551  br2coss  38640  1cosscnvxrn  38677  refsymrels2  38761  dfeqvrels2  38784  dfeldisj5  38919  dnwech  43232  fgraphopab  43387  onfrALTlem5  44725  onfrALTlem4  44726  onfrALTlem5VD  45067  onfrALTlem4VD  45068  disjxp1  45256  disjinfi  45378  oppczeroo  49424