Theorem ineq12i 4211

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

Syntax hints:   = wceq 1542   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3956

This theorem is referenced by:  undir  4277  difundi  4280  difindir  4283  inrab  4307  inrab2  4308  elneldisj  4389  dfif4  4544  dfif5  4545  inxp  5833  resindi  5998  resindir  5999  rnin  6147  inimass  6155  cnvrescnv  6195  predin  6329  funtp  6606  orduniss2  7821  offres  7970  fodomr  9128  epinid0  9595  cnvepnep  9603  wemapwe  9692  cotr3  14925  explecnv  15811  psssdm2  18534  ablfacrp  19936  cnfldfunALT  20957  cnfldfunALTOLD  20958  pjfval2  21264  ofco2  21953  iundisj2  25066  clwwlknondisj  29364  lejdiri  30792  cmbr3i  30853  nonbooli  30904  5oai  30914  3oalem5  30919  mayetes3i  30982  mdexchi  31588  disjpreima  31815  disjxpin  31819  iundisj2f  31821  xppreima  31871  iundisj2fi  32008  xpinpreima  32886  xpinpreima2  32887  ordtcnvNEW  32900  pprodcnveq  34855  dfiota3  34895  bj-inrab  35807  ptrest  36487  ftc1anclem6  36566  xrnres3  37274  br2coss  37308  1cosscnvxrn  37345  refsymrels2  37435  dfeqvrels2  37458  dfeldisj5  37591  dnwech  41790  fgraphopab  41952  onfrALTlem5  43303  onfrALTlem4  43304  onfrALTlem5VD  43646  onfrALTlem4VD  43647  disjxp1  43756  disjinfi  43891