Theorem ineq12 4144

Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)

Assertion

Ref	Expression
ineq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Proof of Theorem ineq12

Step	Hyp	Ref	Expression
1		ineq1 4142	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		ineq2 4143	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷))
3	1, 2	sylan9eq 2794	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 396   = 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:  ineq12i  4147  ineq12d  4150  ineqan12d  4151  fnun  6599  frrlem4  8229  undifixp  8872  endisj  8992  sbthlem8  9022  fiin  9325  pm54.43  9916  kmlem9  10072  indistopon  22984  epttop  22992  restbas  23141  ordtbas2  23174  txbas  23550  ptbasin  23560  trfbas2  23826  snfil  23847  fbasrn  23867  trfil2  23870  fmfnfmlem3  23939  ustuqtop2  24225  minveclem3b  25413  isperp  28798  brredunds  39077  eldisjim3  39182  diophin  43221  kelac2lem  43509  iscnrm3r  49438  incat  50091  setc1onsubc  50092