Theorem ineq12 4032

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 4030	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		ineq2 4031	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∩ 𝐶) = (𝐵 ∩ 𝐷))
3	1, 2	sylan9eq 2834	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∩ cin 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799

This theorem is referenced by:  ineq12i  4035  ineq12d  4038  ineqan12d  4039  fnun  6243  undifixp  8230  endisj  8335  sbthlem8  8365  fiin  8616  pm54.43  9159  kmlem9  9315  indistopon  21213  epttop  21221  restbas  21370  ordtbas2  21403  txbas  21779  ptbasin  21789  trfbas2  22055  snfil  22076  fbasrn  22096  trfil2  22099  fmfnfmlem3  22168  ustuqtop2  22454  minveclem3b  23634  isperp  26063  frrlem4  32372  brreds  34997  diophin  38300  kelac2lem  38597