Theorem ineq12i 4179

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

Syntax hints:   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  undir  4248  difundi  4251  difindir  4254  inrab  4277  inrab2  4278  elneldisj  4356  dfif4  4508  dfif5  4509  resindi  5995  resindir  5996  rninOLD  6145  inimass  6153  cnvrescnv  6195  predin  6329  funtp  6594  orduniss2  7829  offres  7980  fodomr  9116  fodomfir  9287  epinid0  9567  cnvepnep  9577  wemapwe  9666  cotr3  15015  explecnv  15919  psssdm2  18637  ablfacrp  20138  cnfldfunALT  21506  pjfval2  21828  ofco2  22577  iundisj2  25677  clwwlknondisj  30403  lejdiri  31832  cmbr3i  31893  nonbooli  31944  5oai  31954  3oalem5  31959  mayetes3i  32022  mdexchi  32628  disjpreima  32870  disjxpin  32874  iundisj2f  32876  xppreima  32931  iundisj2fi  33083  xpinpreima  34241  xpinpreima2  34242  ordtcnvNEW  34255  pprodcnveq  36272  dfiota3  36312  bj-inrab  37451  ptrest  38158  ftc1anclem6  38237  dmxrn  38926  xrnres3  38966  br2coss  39067  1cosscnvxrn  39104  refsymrels2  39188  dfeqvrels2  39211  dfeldisj5  39352  dnwech  43667  fgraphopab  43822  onfrALTlem5  45143  onfrALTlem4  45144  onfrALTlem5VD  45485  onfrALTlem4VD  45486  disjxp1  45681  disjinfi  45802  oppczeroo  49900