Theorem 3eqtr4i 2831

Description: An inference from three chained equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4i.1	⊢ 𝐴 = 𝐵
3eqtr4i.2	⊢ 𝐶 = 𝐴
3eqtr4i.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
2		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
3		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
4	2, 3	eqtr4i 2824	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2824	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  rabrab  3332  rabbiia  3419  cbvrabw  3437  cbvrab  3438  cbvrabv  3439  cbvcsbw  3838  cbvcsb  3839  csbcow  3843  csbco  3844  cbvrabcsfw  3869  cbvrabcsf  3873  un4  4096  incom  4128  in13  4149  in31  4150  in4  4152  symdifcom  4170  indifcom  4199  indir  4202  undir  4203  difdif2  4211  notrab  4232  dfnul3  4246  dfif5  4441  rabsnifsb  4618  prcom  4628  tprot  4645  tpcoma  4646  tpcomb  4647  tpass  4648  qdassr  4650  pw0  4705  pwpw0  4706  pwsn  4792  pwsnOLD  4793  cbviun  4923  cbviin  4924  cbviung  4925  cbviing  4926  iunrab  4939  iunin1  4957  iinuni  4983  cbvopab  5101  cbvopab1  5103  cbvopab1g  5104  cbvopab2  5105  cbvopab1s  5106  cbvopab2v  5108  unopab  5109  cbvmptf  5129  cbvmptfg  5130  iunopab  5411  dfid4  5426  dfid3  5427  rabxp  5564  fconstmpt  5578  csbxp  5614  inxp  5667  cnvco  5720  csbdm  5730  rnmpt  5791  csbres  5821  resundi  5832  resundir  5833  resindi  5834  resindir  5835  rescom  5844  resima  5852  imadmrn  5906  cnvimarndm  5917  cnvi  5967  cnvin  5970  rnun  5971  imaundi  5975  cnvxp  5981  imainrect  6005  csbrn  6027  imacnvcnv  6030  resdmres  6056  imadmres  6058  mptpreima  6059  dfpred3  6126  predin  6139  predun  6140  preddif  6141  wfi  6149  cbviotaw  6290  cbviota  6292  sb8iota  6294  resdif  6610  opabiotadm  6720  fndmin  6792  fninfp  6913  cbvriotaw  7102  cbvriota  7106  dfoprab2  7191  cbvoprab1  7220  cbvoprab2  7221  cbvoprab12  7222  cbvoprab3  7224  cbvmpox  7226  resoprab  7249  caov32  7355  caov31  7357  caov4  7359  caovlem2  7364  uniuni  7464  zfrep6  7638  ofmres  7667  dfopab2  7732  dfxp3  7741  dmmpossx  7746  fmpox  7747  fsplit  7795  fsplitOLD  7796  ovtpos  7890  tposco  7906  tfrlem10  8006  o2p2e4  8149  o2p2e4OLD  8150  0map0sn0  8432  mapsncnv  8440  cbvixp  8461  xpcomco  8590  sbthlem6  8616  1sdom  8705  cardf2  9356  alephcard  9481  alephfplem1  9515  xp2dju  9587  djuassen  9589  infdju1  9600  pwdju1  9601  ackbij1lem14  9644  compsscnv  9782  dffin1-5  9799  ituniiun  9833  axdc2lem  9859  axdc3lem4  9864  axcclem  9868  pwcfsdom  9994  dmaddpi  10301  dmmulpi  10302  adderpqlem  10365  addassnq  10369  mulcanenq  10371  addcmpblnr  10480  mulcmpblnrlem  10481  ltsrpr  10488  mulgt0sr  10516  sqgt0sr  10517  axi2m1  10570  negiso  11608  nummac  12131  decsubi  12149  9t11e99  12216  fztpval  12964  seqval  13375  sqrecii  13542  sqdivi  13544  binom2i  13570  4bc2eq6  13685  hashgval  13689  revs1  14118  cats1cat  14214  trclublem  14346  shftdm  14422  shftidt2  14432  cji  14510  cbvsum  15044  sumfc  15058  ackbijnn  15175  cbvprod  15261  prodfc  15291  fsumcube  15406  divalglem2  15736  nn0gcdsq  16082  prmreclem2  16243  prmrec  16248  hashbc0  16331  dec5nprm  16392  dec2nprm  16393  gcdi  16399  decexp2  16401  decsplit  16409  1259lem1  16456  1259lem4  16459  4001lem1  16466  phlstr  16645  lubdm  17581  glbdm  17594  oduval  17732  oduleval  17733  odubas  17735  oppgid  18476  symgbas0  18509  gsumcom2  19088  ringidval  19246  oppr1  19380  dfrhm2  19465  rmodislmod  19695  cnfldsub  20119  cnflddiv  20121  dvdsrzring  20176  pjdm  20396  pjfval2  20398  opsrtoslem1  20723  restco  21769  ufprim  22514  tgioo3  23410  oprpiece1res1  23556  oprpiece1res2  23557  volfiniun  24151  vitalilem4  24215  cbvitg  24379  itgresr  24382  cbvditg  24457  plyid  24806  coeidp  24860  dgrid  24861  sincos3rdpi  25109  logblog  25378  ang180lem2  25396  1cubrlem  25427  asin1  25480  log2ublem2  25533  log2ublem3  25534  emcllem5  25585  lgsdir2lem5  25913  lgsquadlem3  25966  2lgslem1b  25976  2lgsoddprmlem3d  25997  cchhllem  26681  ax5seglem7  26729  vtxval0  26832  iedgval0  26833  finsumvtxdg2ssteplem1  27335  wwlksnfi  27692  1wlkdlem1  27922  ex-un  28209  ex-pw  28214  ex-cnv  28222  ex-co  28223  bafval  28387  vsfval  28416  cnnvba  28462  cnnvm  28465  ip2dii  28627  siilem1  28634  h2hcau  28762  hvsubsub4i  28842  hvnegdii  28845  normlem3  28895  normlem8  28900  norm-iii-i  28922  normpar2i  28939  polid2i  28940  chjassi  29269  chj4i  29306  h1de2i  29336  spanunsni  29362  fh3i  29406  fh4i  29407  qlax4i  29413  qlaxr3i  29419  3oalem5  29449  pjadjii  29457  pjsubii  29461  hoadd32i  29561  cnvadj  29675  hh0oi  29686  hhcno  29687  hhcnf  29688  nmopnegi  29748  lnophmlem2  29800  branmfn  29888  dmrab  30267  abrexexd  30277  cbviunf  30319  maprnin  30493  dpmul10  30597  dpexpp1  30610  dpadd3  30614  dpmul  30615  dpmul4  30616  psgnfzto1st  30797  cycpmconjs  30848  lmlimxrge0  31301  zrhre  31370  qqhre  31371  rrhre  31372  cbvesum  31411  unibrsiga  31555  eulerpartlemt  31739  eulerpartgbij  31740  ballotlemrinv  31901  hgt750lem2  32033  bnj1146  32173  bnj893  32310  bnj1234  32395  subfacp1lem1  32539  kur14lem2  32567  kur14lem5  32570  kur14lem7  32572  cvmscld  32633  satfv1lem  32722  fmla0  32742  mvtval  32860  mthmpps  32942  frpoind  33193  frind  33198  frrlem5  33240  noextend  33286  nosupbday  33318  nosupbnd1  33327  nosupbnd2  33329  dmscut  33385  madeval2  33403  fixun  33483  bj-inrab  34369  bj-inrab3  34371  bj-pr1un  34439  bj-pr2un  34453  bj-mpomptALT  34534  rnmptsn  34752  f1omptsnlem  34753  rabiun  35030  phpreu  35041  poimirlem18  35075  ovoliunnfl  35099  voliunnfl  35101  mbfposadd  35104  asindmre  35140  abeqin  35674  rncnvepres  35721  qsresid  35742  rnxrn  35806  xrnres  35810  xrnres2  35811  xrnres3  35812  rncossdmcoss  35855  1cosscnvxrn  35875  refrelsredund4  36027  cdleme25cv  37654  sqdeccom12  39483  nn0expgcd  39492  sn-00idlem2  39537  sn-1ticom  39571  mendsca  40133  areaquad  40166  cnvrcl0  40325  sqrtcvallem1  40331  trclrelexplem  40412  df3o2  40727  df3o3  40728  cbvmpo2  41733  cbvmpo1  41734  mptssid  41877  fprodabs2  42237  stoweidlem13  42655  wallispilem4  42710  fourierdlem94  42842  fourierdlem102  42850  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fourierdlem114  42862  41prothprmlem2  44136  2exp340mod341  44251  8exp8mod9  44254  nfermltl8rev  44260  cbvmpox2  44737  dmmpossx2  44738  zlmodzxzequa  44905  zlmodzxzequap  44908