Theorem ineq12d 4144

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  csbin  4370  predeq123  6192  funcnvtp  6481  ofrfvalg  7519  offval  7520  oev2  8315  isf32lem7  10046  ressval  16870  invffval  17387  invfval  17388  dfiso2  17401  isofn  17404  oppcinv  17409  zerooval  17626  cat1  17728  isps  18201  dmdprd  19516  dprddisj  19527  dprdf1o  19550  dmdprdsplit2lem  19563  dmdprdpr  19567  pgpfaclem1  19599  isunit  19814  dfrhm2  19876  isrhm  19880  2idlval  20417  pjfval  20823  aspval  20987  ressmplbas2  21138  isconn  22472  connsuba  22479  ptbasin  22636  ptclsg  22674  qtopval  22754  rnelfmlem  23011  trust  23289  isnmhm  23816  uniioombllem2a  24651  dyaddisjlem  24664  dyaddisj  24665  i1faddlem  24762  i1fmullem  24763  limcflf  24950  ewlksfval  27871  isewlk  27872  ewlkinedg  27874  ispth  27992  trlsegvdeg  28492  frcond3  28534  numclwwlk3lem2  28649  chocin  29758  cmbr3  29871  pjoml3  29875  fh1  29881  fnunres1  30846  xppreima2  30889  cosnopne  30929  swrdrndisj  31131  hauseqcn  31750  prsssdm  31769  ordtrestNEW  31773  ordtrest2NEW  31775  cndprobval  32300  ballotlemfrc  32393  bnj1421  32922  satffunlem  33263  satffunlem1lem2  33265  satffunlem2lem1  33266  satffunlem2lem2  33268  msrval  33400  msrf  33404  ismfs  33411  clsun  34444  poimirlem8  35712  itg2addnclem2  35756  heiborlem4  35899  heiborlem6  35901  heiborlem10  35905  pmodl42N  37792  polfvalN  37845  poldmj1N  37869  pmapj2N  37870  pnonsingN  37874  psubclinN  37889  poml4N  37894  osumcllem9N  37905  trnfsetN  38096  diainN  38998  djaffvalN  39074  djafvalN  39075  djajN  39078  dihmeetcl  39286  dihmeet2  39287  dochnoncon  39332  djhffval  39337  djhfval  39338  djhlj  39342  dochdmm1  39351  lclkrlem2g  39454  lclkrlem2v  39469  lcfrlem21  39504  lcfrlem24  39507  mapdunirnN  39591  baerlem5amN  39657  baerlem5bmN  39658  baerlem5abmN  39659  mapdheq4lem  39672  mapdh6lem1N  39674  mapdh6lem2N  39675  hdmap1l6lem1  39748  hdmap1l6lem2  39749  aomclem8  40802  disjrnmpt2  42615  dvsinax  43344  dvcosax  43357  nnfoctbdjlem  43883  smfpimcc  44228  smfsuplem2  44232  rhmval  45365  iscnrm3l  46133