Theorem ineq12 4134

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888

This theorem is referenced by:  ineq12i  4137  ineq12d  4140  ineqan12d  4141  fnun  6434  undifixp  8481  endisj  8587  sbthlem8  8618  fiin  8870  pm54.43  9414  kmlem9  9569  indistopon  21606  epttop  21614  restbas  21763  ordtbas2  21796  txbas  22172  ptbasin  22182  trfbas2  22448  snfil  22469  fbasrn  22489  trfil2  22492  fmfnfmlem3  22561  ustuqtop2  22848  minveclem3b  24032  isperp  26506  frrlem4  33239  brredunds  36021  diophin  39713  kelac2lem  40008