Theorem ineq12 4236

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  ineq12i  4239  ineq12d  4242  ineqan12d  4243  fnun  6693  frrlem4  8330  undifixp  8992  endisj  9124  sbthlem8  9156  fiin  9491  pm54.43  10070  kmlem9  10228  indistopon  23029  epttop  23037  restbas  23187  ordtbas2  23220  txbas  23596  ptbasin  23606  trfbas2  23872  snfil  23893  fbasrn  23913  trfil2  23916  fmfnfmlem3  23985  ustuqtop2  24272  minveclem3b  25481  isperp  28738  brredunds  38582  diophin  42728  kelac2lem  43021  iscnrm3r  48628