Theorem ineq12i 4147

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

Syntax hints:   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  undir  4215  difundi  4218  difindir  4221  inrab  4244  inrab2  4245  elneldisj  4320  dfif4  4470  dfif5  4471  resindi  5947  resindir  5948  rnin  6097  inimass  6106  cnvrescnv  6146  predin  6278  funtp  6542  orduniss2  7773  offres  7925  fodomr  9056  fodomfir  9228  epinid0  9510  cnvepnep  9520  wemapwe  9609  cotr3  14931  explecnv  15821  psssdm2  18538  ablfacrp  20034  cnfldfunALT  21362  pjfval2  21684  ofco2  22434  iundisj2  25534  clwwlknondisj  30199  lejdiri  31628  cmbr3i  31689  nonbooli  31740  5oai  31750  3oalem5  31755  mayetes3i  31818  mdexchi  32424  disjpreima  32673  disjxpin  32677  iundisj2f  32679  xppreima  32737  iundisj2fi  32889  xpinpreima  34090  xpinpreima2  34091  ordtcnvNEW  34104  pprodcnveq  36109  dfiota3  36149  bj-inrab  37280  ptrest  37986  ftc1anclem6  38065  dmxrn  38754  xrnres3  38794  br2coss  38895  1cosscnvxrn  38932  refsymrels2  39016  dfeqvrels2  39039  dfeldisj5  39180  dnwech  43493  fgraphopab  43648  onfrALTlem5  44986  onfrALTlem4  44987  onfrALTlem5VD  45328  onfrALTlem4VD  45329  disjxp1  45517  disjinfi  45639  oppczeroo  49727