Theorem ineq12 4147

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542   ∩ cin 3891

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-in 3899

This theorem is referenced by:  ineq12i  4150  ineq12d  4153  ineqan12d  4154  fnun  6542  frrlem4  8094  undifixp  8703  endisj  8826  sbthlem8  8857  fiin  9157  pm54.43  9758  kmlem9  9913  indistopon  22147  epttop  22155  restbas  22305  ordtbas2  22338  txbas  22714  ptbasin  22724  trfbas2  22990  snfil  23011  fbasrn  23031  trfil2  23034  fmfnfmlem3  23103  ustuqtop2  23390  minveclem3b  24588  isperp  27069  brredunds  36733  diophin  40589  kelac2lem  40884  iscnrm3r  46209