Theorem ineq12d 4104

Description: Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
ineq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
ineq12d	⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Proof of Theorem ineq12d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		ineq12 4098	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3842

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 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-in 3850

This theorem is referenced by:  csbin  4329  predeq123  6130  funcnvtp  6402  ofrfvalg  7432  offval  7433  oev2  8179  isf32lem7  9859  ressval  16654  invffval  17133  invfval  17134  dfiso2  17147  isofn  17150  oppcinv  17155  zerooval  17367  cat1  17469  isps  17928  dmdprd  19239  dprddisj  19250  dprdf1o  19273  dmdprdsplit2lem  19286  dmdprdpr  19290  pgpfaclem1  19322  isunit  19529  dfrhm2  19591  isrhm  19595  2idlval  20125  pjfval  20522  aspval  20686  ressmplbas2  20838  isconn  22164  connsuba  22171  ptbasin  22328  ptclsg  22366  qtopval  22446  rnelfmlem  22703  trust  22981  isnmhm  23499  uniioombllem2a  24334  dyaddisjlem  24347  dyaddisj  24348  i1faddlem  24445  i1fmullem  24446  limcflf  24633  ewlksfval  27543  isewlk  27544  ewlkinedg  27546  ispth  27664  trlsegvdeg  28164  frcond3  28206  numclwwlk3lem2  28321  chocin  29430  cmbr3  29543  pjoml3  29547  fh1  29553  fnunres1  30519  xppreima2  30562  cosnopne  30602  swrdrndisj  30804  hauseqcn  31420  prsssdm  31439  ordtrestNEW  31443  ordtrest2NEW  31445  cndprobval  31970  ballotlemfrc  32063  bnj1421  32593  satffunlem  32934  satffunlem1lem2  32936  satffunlem2lem1  32937  satffunlem2lem2  32939  msrval  33071  msrf  33075  ismfs  33082  clsun  34155  poimirlem8  35408  itg2addnclem2  35452  heiborlem4  35595  heiborlem6  35597  heiborlem10  35601  pmodl42N  37488  polfvalN  37541  poldmj1N  37565  pmapj2N  37566  pnonsingN  37570  psubclinN  37585  poml4N  37590  osumcllem9N  37601  trnfsetN  37792  diainN  38694  djaffvalN  38770  djafvalN  38771  djajN  38774  dihmeetcl  38982  dihmeet2  38983  dochnoncon  39028  djhffval  39033  djhfval  39034  djhlj  39038  dochdmm1  39047  lclkrlem2g  39150  lclkrlem2v  39165  lcfrlem21  39200  lcfrlem24  39203  mapdunirnN  39287  baerlem5amN  39353  baerlem5bmN  39354  baerlem5abmN  39355  mapdheq4lem  39368  mapdh6lem1N  39370  mapdh6lem2N  39371  hdmap1l6lem1  39444  hdmap1l6lem2  39445  aomclem8  40458  disjrnmpt2  42264  dvsinax  42996  dvcosax  43009  nnfoctbdjlem  43535  smfpimcc  43880  smfsuplem2  43884  rhmval  45011  iscnrm3l  45767