Theorem ineq12d 4192

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 4186	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))
4	1, 2, 3	syl2anc 586	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-in 3945

This theorem is referenced by:  csbin  4393  predeq123  6151  funcnvtp  6419  offval  7418  ofrfval  7419  oev2  8150  isf32lem7  9783  ressval  16553  invffval  17030  invfval  17031  dfiso2  17044  isofn  17047  oppcinv  17052  zerooval  17261  isps  17814  dmdprd  19122  dprddisj  19133  dprdf1o  19156  dmdprdsplit2lem  19169  dmdprdpr  19173  pgpfaclem1  19205  isunit  19409  dfrhm2  19471  isrhm  19475  2idlval  20008  aspval  20104  ressmplbas2  20238  pjfval  20852  isconn  22023  connsuba  22030  ptbasin  22187  ptclsg  22225  qtopval  22305  rnelfmlem  22562  trust  22840  isnmhm  23357  uniioombllem2a  24185  dyaddisjlem  24198  dyaddisj  24199  i1faddlem  24296  i1fmullem  24297  limcflf  24481  ewlksfval  27385  isewlk  27386  ewlkinedg  27388  ispth  27506  trlsegvdeg  28008  frcond3  28050  numclwwlk3lem2  28165  chocin  29274  cmbr3  29387  pjoml3  29391  fh1  29397  fnunres1  30358  xppreima2  30397  cosnopne  30432  swrdrndisj  30633  hauseqcn  31140  prsssdm  31162  ordtrestNEW  31166  ordtrest2NEW  31168  cndprobval  31693  ballotlemfrc  31786  bnj1421  32316  satffunlem  32650  satffunlem1lem2  32652  satffunlem2lem1  32653  satffunlem2lem2  32655  msrval  32787  msrf  32791  ismfs  32798  clsun  33678  poimirlem8  34902  itg2addnclem2  34946  heiborlem4  35094  heiborlem6  35096  heiborlem10  35100  pmodl42N  36989  polfvalN  37042  poldmj1N  37066  pmapj2N  37067  pnonsingN  37071  psubclinN  37086  poml4N  37091  osumcllem9N  37102  trnfsetN  37293  diainN  38195  djaffvalN  38271  djafvalN  38272  djajN  38275  dihmeetcl  38483  dihmeet2  38484  dochnoncon  38529  djhffval  38534  djhfval  38535  djhlj  38539  dochdmm1  38548  lclkrlem2g  38651  lclkrlem2v  38666  lcfrlem21  38701  lcfrlem24  38704  mapdunirnN  38788  baerlem5amN  38854  baerlem5bmN  38855  baerlem5abmN  38856  mapdheq4lem  38869  mapdh6lem1N  38871  mapdh6lem2N  38872  hdmap1l6lem1  38945  hdmap1l6lem2  38946  aomclem8  39668  disjrnmpt2  41456  dvsinax  42204  dvcosax  42218  nnfoctbdjlem  42744  smfpimcc  43089  smfsuplem2  43093  rhmval  44197