Theorem ineq12i 4217

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

Syntax hints:   = wceq 1539   ∩ cin 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-in 3957

This theorem is referenced by:  undir  4286  difundi  4289  difindir  4292  inrab  4315  inrab2  4316  elneldisj  4391  dfif4  4540  dfif5  4541  inxpOLD  5842  resindi  6012  resindir  6013  rnin  6165  inimass  6174  cnvrescnv  6214  predin  6347  funtp  6622  orduniss2  7854  offres  8009  fodomr  9169  fodomfir  9369  epinid0  9641  cnvepnep  9649  wemapwe  9738  cotr3  15018  explecnv  15902  psssdm2  18627  ablfacrp  20087  cnfldfunALT  21380  cnfldfunALTOLD  21393  cnfldfunALTOLDOLD  21394  pjfval2  21730  ofco2  22458  iundisj2  25585  clwwlknondisj  30131  lejdiri  31559  cmbr3i  31620  nonbooli  31671  5oai  31681  3oalem5  31686  mayetes3i  31749  mdexchi  32355  disjpreima  32598  disjxpin  32602  iundisj2f  32604  xppreima  32656  iundisj2fi  32800  xpinpreima  33906  xpinpreima2  33907  ordtcnvNEW  33920  pprodcnveq  35885  dfiota3  35925  bj-inrab  36929  ptrest  37627  ftc1anclem6  37706  xrnres3  38406  br2coss  38440  1cosscnvxrn  38477  refsymrels2  38567  dfeqvrels2  38590  dfeldisj5  38723  dnwech  43065  fgraphopab  43220  onfrALTlem5  44567  onfrALTlem4  44568  onfrALTlem5VD  44910  onfrALTlem4VD  44911  disjxp1  45079  disjinfi  45202