Theorem ineq12i 3845

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

Syntax hints:   = wceq 1523   ∩ cin 3606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614

This theorem is referenced by:  undir  3909  difundi  3912  difindir  3915  inrab  3932  inrab2  3933  elneldisj  3996  elneldisjOLD  3998  dfif4  4134  dfif5  4135  inxp  5287  resindi  5447  resindir  5448  rnin  5577  inimass  5584  predin  5741  funtp  5983  orduniss2  7075  offres  7205  fodomr  8152  wemapwe  8632  cotr3  13763  explecnv  14641  psssdm2  17262  ablfacrp  18511  cnfldfun  19806  pjfval2  20101  ofco2  20305  iundisj2  23363  clwwlknondisj  27086  lejdiri  28526  cmbr3i  28587  nonbooli  28638  5oai  28648  3oalem5  28653  mayetes3i  28716  mdexchi  29322  disjpreima  29523  disjxpin  29527  iundisj2f  29529  xppreima  29577  iundisj2fi  29684  xpinpreima  30080  xpinpreima2  30081  ordtcnvNEW  30094  pprodcnveq  32115  dfiota3  32155  bj-inrab  33048  ptrest  33538  ftc1anclem6  33620  xrnres3  34302  br2coss  34333  1cosscnvxrn  34365  refsymrels2  34449  dnwech  37935  fgraphopab  38105  onfrALTlem5  39074  onfrALTlem4  39075  onfrALTlem5VD  39435  onfrALTlem4VD  39436  disjxp1  39552  disjinfi  39694