Theorem 3eqtr4i 2654

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	|- A = B
3eqtr4i.2	|- C = A
3eqtr4i.3	|- D = B

Assertion

Ref	Expression
3eqtr4i	|- C = D

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 |- C = A
2		3eqtr4i.3	. . 3 |- D = B
3		3eqtr4i.1	. . 3 |- A = B
4	2, 3	eqtr4i 2647	. 2 |- D = A
5	1, 4	eqtr4i 2647	1 |- C = D

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  rabswap  3121  rabbiia  3185  cbvrab  3198  cbvcsb  3538  csbco  3543  cbvrabcsf  3568  un4  3773  in13  3826  in31  3827  in4  3829  symdifcom  3845  indifcom  3872  indir  3875  undir  3876  difdif2  3884  notrab  3904  dfnul3  3918  rab0OLD  3956  dfif5  4102  rabsnifsb  4257  prcom  4267  tprot  4284  tpcoma  4285  tpcomb  4286  tpass  4287  qdassr  4289  pw0  4343  pwpw0  4344  pwsn  4428  pwsnALT  4429  int0OLD  4491  cbviun  4557  cbviin  4558  iunrab  4567  iunin1  4585  iinuni  4609  cbvopab  4721  cbvopab1  4723  cbvopab2  4724  cbvopab1s  4725  cbvopab2v  4727  unopab  4728  cbvmptf  4748  cbvmpt  4749  iunopab  5012  dfid3  5025  dfid4  5026  rabxp  5154  fconstmpt  5163  csbxp  5200  inxp  5254  cnvco  5308  csbdm  5318  rnmpt  5371  csbres  5399  resundi  5410  resundir  5411  resindi  5412  resindir  5413  rescom  5423  resima  5431  imadmrn  5476  cnvimarndm  5486  cnvi  5537  cnvin  5540  rnun  5541  imaundi  5545  cnvxp  5551  imainrect  5575  csbrn  5596  imacnvcnv  5599  resdmres  5625  imadmres  5627  mptpreima  5628  dfpred3  5690  predin  5703  predun  5704  preddif  5705  wfi  5713  cbviota  5856  sb8iota  5858  resdif  6157  opabiotadm  6260  fndmin  6324  fninfp  6440  cbvriota  6621  dfoprab2  6701  cbvoprab1  6727  cbvoprab2  6728  cbvoprab12  6729  cbvoprab3  6731  cbvmpt2x  6733  resoprab  6756  caov32  6861  caov31  6863  caov4  6865  caovlem2  6870  uniuni  6971  zfrep6  7134  ofmres  7164  dfopab2  7222  dfxp3  7230  dmmpt2ssx  7235  fmpt2x  7236  fsplit  7282  ovtpos  7367  tposco  7383  tfrlem10  7483  o2p2e4  7621  mapsncnv  7904  cbvixp  7925  xpcomco  8050  sbthlem6  8075  1sdom  8163  cardf2  8769  alephcard  8893  alephfplem1  8927  pwcda1  9016  ackbij1lem14  9055  compsscnv  9193  dffin1-5  9210  ituniiun  9244  axdc2lem  9270  axdc3lem4  9275  axcclem  9279  pwcfsdom  9405  dmaddpi  9712  dmmulpi  9713  adderpqlem  9776  addassnq  9780  mulcanenq  9782  addcmpblnr  9890  mulcmpblnrlem  9891  ltsrpr  9898  mulgt0sr  9926  sqgt0sr  9927  axi2m1  9980  negiso  11003  nummac  11558  decsubi  11583  decsubiOLD  11584  9t11e99  11671  9t11e99OLD  11672  fzprval  12401  fztpval  12402  seqval  12812  sqrecii  12946  sqdivi  12948  binom2i  12974  4bc2eq6  13116  hashgval  13120  revs1  13514  cats1cat  13606  trclublem  13734  shftdm  13811  shftidt2  13821  cji  13899  cbvsum  14425  sumfc  14440  ackbijnn  14560  cbvprod  14645  prodfc  14675  fsumcube  14791  divalglem2  15118  nn0gcdsq  15460  prmreclem2  15621  prmrec  15626  hashbc0  15709  dec5nprm  15770  dec2nprm  15771  gcdi  15777  decexp2  15779  decsplit  15787  decsplitOLD  15791  1259lem1  15838  1259lem4  15841  4001lem1  15848  dfpleOLD  15962  strlemor2OLD  15970  strlemor3OLD  15971  phlstr  16034  lubdm  16979  glbdm  16992  oduval  17130  oduleval  17131  odubas  17133  oppgid  17786  symgbas0  17814  gsumcom2  18374  ringidval  18503  oppr1  18634  dfrhm2  18717  rmodislmod  18931  opsrtoslem1  19484  cnfldsub  19774  cnflddiv  19776  dvdsrzring  19831  pjdm  20051  pjfval2  20053  restco  20968  cnmptid  21464  ufprim  21713  tgioo3  22608  oprpiece1res1  22750  oprpiece1res2  22751  volfiniun  23315  vitalilem4  23380  cbvitg  23542  itgresr  23545  iblcnlem1  23554  cbvditg  23618  sincos3rdpi  24268  logblog  24530  ang180lem2  24540  1cubrlem  24568  asin1  24621  log2ublem2  24674  log2ublem3  24675  emcllem5  24726  lgsdir2lem5  25054  lgsquadlem3  25107  2lgslem1b  25117  2lgsoddprmlem3d  25138  cchhllem  25767  ax5seglem7  25815  axlowdimlem4  25825  vtxval0  25931  iedgval0  25932  finsumvtxdg2ssteplem1  26441  1wlkdlem1  26997  ex-un  27281  ex-pw  27286  ex-cnv  27294  ex-co  27295  bafval  27459  vsfval  27488  cnnvba  27534  cnnvm  27537  ip2dii  27699  siilem1  27706  h2hcau  27836  hvsubsub4i  27916  hvnegdii  27919  normlem3  27969  normlem8  27974  norm-iii-i  27996  normpar2i  28013  polid2i  28014  chjassi  28345  chj4i  28382  h1de2i  28412  spanunsni  28438  fh3i  28482  fh4i  28483  qlax4i  28489  qlaxr3i  28495  3oalem5  28525  pjadjii  28533  pjsubii  28537  hoadd32i  28637  cnvadj  28751  hh0oi  28762  hhcno  28763  hhcnf  28764  nmopnegi  28824  lnophmlem2  28876  branmfn  28964  rabrab  29338  abrexexd  29347  cbviunf  29372  maprnin  29506  dpmul10  29603  dpexpp1  29616  dpadd3  29620  dpmul  29621  dpmul4  29622  psgnfzto1st  29855  lmlimxrge0  29994  rrhre  30065  cbvesum  30104  unibrsiga  30249  eulerpartlemt  30433  eulerpartgbij  30434  ballotlem2  30550  ballotlemrinv  30595  hgt750lem2  30730  bnj1146  30862  bnj893  30998  bnj1234  31081  subfacp1lem1  31161  kur14lem2  31189  kur14lem5  31192  kur14lem7  31194  cvmscld  31255  mvtval  31397  mthmpps  31479  frind  31740  noextend  31819  nosupbday  31851  nosupbnd1  31860  nosupbnd2  31862  dmscut  31918  madeval2  31936  fixun  32016  bj-inrab  32923  bj-inrab3  32925  bj-pr1un  32991  bj-pr2un  33005  bj-mpt2mptALT  33072  f1omptsnlem  33183  rabiun  33382  phpreu  33393  poimirlem18  33427  ovoliunnfl  33451  voliunnfl  33453  mbfposadd  33457  asindmre  33495  abeqin  34017  rncnvepres  34073  qsresid  34096  cdleme25cv  35646  mendsca  37759  areaquad  37802  cnvrcl0  37932  trclrelexplem  38003  df3o2  38322  df3o3  38323  cbvmpt22  39277  cbvmpt21  39278  mptssid  39450  fprodabs2  39827  stoweidlem13  40230  wallispilem4  40285  fourierdlem94  40417  fourierdlem102  40425  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fourierdlem114  40437  41prothprmlem2  41535  cbvmpt2x2  42114  dmmpt2ssx2  42115  zlmodzxzequa  42285  zlmodzxzequap  42288