Theorem 3eqtr4i 2775

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 2768	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2768	1 ⊢ 𝐶 = 𝐷

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  rabbiiaOLD  3441  cbvrabv  3447  rabrab  3461  cbvrabw  3473  cbvrabwOLD  3474  cbvrab  3479  cbvcsbw  3909  cbvcsb  3910  cbvcsbv  3911  csbcow  3914  csbco  3915  cbvrabcsfw  3940  cbvrabcsf  3944  un4  4175  incom  4209  in13  4231  in31  4232  in4  4234  symdifcom  4254  indifcom  4283  indir  4286  undir  4287  indifdir  4295  difdif2  4296  notrab  4322  dfnul3  4337  dfif5  4542  rabsnifsb  4722  prcom  4732  tprot  4749  tpcoma  4750  tpcomb  4751  tpass  4752  qdassr  4754  pw0  4812  pwpw0  4813  pwsn  4900  cbviun  5036  cbviin  5037  cbviung  5038  cbviing  5039  cbviunv  5040  cbviinv  5041  iunrab  5052  iunin1  5072  iinuni  5098  cbvopab  5215  cbvopabv  5216  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  cbvopab1v  5221  cbvopab2v  5223  unopab  5224  cbvmptf  5251  cbvmptfg  5252  cbvmptv  5255  iunopab  5564  iunopabOLD  5565  dfid4  5579  dfid2  5580  dfid3  5581  rabxp  5733  fconstmpt  5747  csbxp  5785  inxpOLD  5843  cnvco  5896  csbdm  5908  rnmpt  5968  csbres  6000  resundi  6011  resundir  6012  resindi  6013  resindir  6014  rescom  6020  resima  6033  imadmrn  6088  cnvimarndm  6101  cnvi  6161  cnvin  6164  rnun  6165  imaundi  6169  cnvxp  6177  imainrect  6201  csbrn  6223  imacnvcnv  6226  resdmres  6252  imadmres  6254  resdifdir  6257  mptpreima  6258  dfpred3  6332  predin  6348  predun  6349  preddif  6350  frpoind  6363  wfiOLD  6372  cbviotaw  6521  cbviotavw  6522  cbviota  6523  sb8iota  6525  resdif  6869  opabiotadm  6990  fndmin  7065  fninfp  7194  cbvriotaw  7397  cbvriotavw  7398  cbvriota  7401  riotarab  7430  dfoprab2  7491  cbvoprab1  7520  cbvoprab2  7521  cbvoprab12  7522  cbvoprab12v  7523  cbvoprab3  7524  cbvoprab3v  7525  cbvmpox  7526  cbvmpov  7528  resoprab  7551  caov32  7660  caov31  7662  caov4  7664  caovlem2  7669  uniuni  7782  zfrep6  7979  ofmres  8009  dfopab2  8077  dfxp3  8086  dmmpossx  8091  fmpox  8092  fsplit  8142  ovtpos  8266  tposco  8282  frrlem5  8315  tfrlem10  8427  o2p2e4  8579  0map0sn0  8925  mapsncnv  8933  cbvixp  8954  cbvixpv  8955  xpcomco  9102  sbthlem6  9128  1sdomOLD  9285  ttrclresv  9757  frind  9790  cardf2  9983  alephcard  10110  alephfplem1  10144  xp2dju  10217  djuassen  10219  infdju1  10230  pwdju1  10231  ackbij1lem14  10272  compsscnv  10411  dffin1-5  10428  ituniiun  10462  axdc2lem  10488  axdc3lem4  10493  axcclem  10497  pwcfsdom  10623  dmaddpi  10930  dmmulpi  10931  adderpqlem  10994  addassnq  10998  mulcanenq  11000  addcmpblnr  11109  mulcmpblnrlem  11110  ltsrpr  11117  mulgt0sr  11145  sqgt0sr  11146  axi2m1  11199  negiso  12248  nummac  12778  decsubi  12796  9t11e99  12863  fztpval  13626  seqval  14053  sqrecii  14222  sqdivi  14224  binom2i  14251  4bc2eq6  14368  hashgval  14372  revs1  14803  cats1cat  14900  trclublem  15034  shftdm  15110  shftidt2  15120  cji  15198  cbvsum  15731  cbvsumv  15732  sumfc  15745  ackbijnn  15864  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  prodfc  15981  fsumcube  16096  divalglem2  16432  nn0expgcd  16601  nn0gcdsq  16789  prmreclem2  16955  prmrec  16960  hashbc0  17043  dec5nprm  17104  dec2nprm  17105  gcdi  17111  decsplit  17120  1259lem1  17168  1259lem4  17171  4001lem1  17178  phlstr  17390  oduval  18333  oduleval  18334  odubas  18336  odubasOLD  18337  lubdm  18396  glbdm  18409  oppgid  19375  symgbas0  19406  gsumcom2  19993  ringidval  20180  oppr1  20350  dfrhm2  20474  rmodislmod  20928  cnfldsub  21410  cnflddiv  21413  cnflddivOLD  21414  dvdsrzring  21472  pjdm  21727  pjfval2  21729  opsrtoslem1  22079  restco  23172  ufprim  23917  tgioo3  24827  oprpiece1res1  24982  oprpiece1res2  24983  volfiniun  25582  vitalilem4  25646  cbvitg  25811  cbvitgv  25812  itgresr  25814  cbvditg  25889  plyid  26248  coeidp  26303  dgrid  26304  sincos3rdpi  26559  logblog  26835  ang180lem2  26853  1cubrlem  26884  asin1  26937  log2ublem2  26990  log2ublem3  26991  emcllem5  27043  lgsdir2lem5  27373  lgsquadlem3  27426  2lgslem1b  27436  2lgsoddprmlem3d  27457  noextend  27711  nosupbday  27750  nosupbnd1  27759  nosupbnd2  27761  noinfbday  27765  noinfbnd1  27774  dmscut  27856  madeval2  27892  negs0s  28058  negs1s  28059  1p1e2s  28400  cchhllem  28901  cchhllemOLD  28902  ax5seglem7  28950  vtxval0  29056  iedgval0  29057  finsumvtxdg2ssteplem1  29563  wwlksnfi  29926  1wlkdlem1  30156  ex-un  30443  ex-pw  30448  ex-cnv  30456  ex-co  30457  bafval  30623  vsfval  30652  cnnvba  30698  cnnvm  30701  ip2dii  30863  siilem1  30870  h2hcau  30998  hvsubsub4i  31078  hvnegdii  31081  normlem3  31131  normlem8  31136  norm-iii-i  31158  normpar2i  31175  polid2i  31176  chjassi  31505  chj4i  31542  h1de2i  31572  spanunsni  31598  fh3i  31642  fh4i  31643  qlax4i  31649  qlaxr3i  31655  3oalem5  31685  pjadjii  31693  pjsubii  31697  hoadd32i  31797  cnvadj  31911  hh0oi  31922  hhcno  31923  hhcnf  31924  nmopnegi  31984  lnophmlem2  32036  branmfn  32124  dmrab  32516  3unrab  32522  abrexexd  32528  cbviunf  32568  maprnin  32742  dpmul10  32877  dpexpp1  32890  dpadd3  32894  dpmul  32895  dpmul4  32896  psgnfzto1st  33125  cycpmconjs  33176  fracbas  33307  lmlimxrge0  33947  zrhre  34020  qqhre  34021  rrhre  34022  cbvesum  34043  cbvesumv  34044  unibrsiga  34187  eulerpartlemt  34373  eulerpartgbij  34374  ballotlemrinv  34536  hgt750lem2  34667  bnj1146  34805  bnj893  34942  bnj1234  35027  subfacp1lem1  35184  kur14lem2  35212  kur14lem5  35215  kur14lem7  35217  cvmscld  35278  satfv1lem  35367  fmla0  35387  mvtval  35505  mthmpps  35587  fixun  35910  rabeqbii  36195  iuneq12i  36196  iineq1i  36197  iineq12i  36198  riotaeqbii  36199  ixpeq1i  36201  sumeq2si  36203  prodeq2si  36205  itgeq12i  36207  ditgeq123i  36210  cbvcsbvw2  36232  cbviunvw2  36233  cbviinvw2  36234  cbvmptvw2  36235  cbvriotavw2  36237  cbvoprab1vw  36238  cbvoprab2vw  36239  cbvoprab123vw  36240  cbvoprab23vw  36241  cbvoprab13vw  36242  cbvmpovw2  36243  cbvmpo1vw2  36244  cbvmpo2vw2  36245  cbvixpvw2  36246  cbvprodvw2  36248  cbvitgvw2  36249  cbvditgvw2  36250  bj-inrab  36928  bj-inrab3  36930  bj-gabeqis  36939  bj-pr1un  37004  bj-pr2un  37018  bj-dfid2ALT  37066  bj-mpomptALT  37120  rnmptsn  37336  f1omptsnlem  37337  rabiun  37600  phpreu  37611  poimirlem18  37645  ovoliunnfl  37669  voliunnfl  37671  mbfposadd  37674  asindmre  37710  abeqin  38253  rncnvepres  38304  qsresid  38326  rnxrn  38399  xrnres  38403  xrnres2  38404  xrnres3  38405  rncossdmcoss  38456  1cosscnvxrn  38476  refrelsredund4  38633  mpets  38843  cdleme25cv  40360  sn-iotalemcor  42261  sqdeccom12  42324  sumcubes  42347  resuppsinopn  42393  sn-00idlem2  42429  sn-1ticom  42464  mendsca  43197  areaquad  43228  onsucrn  43284  df3o2  43326  df3o3  43327  omcl3g  43347  dfno2  43441  cnvrcl0  43638  sqrtcvallem1  43644  trclrelexplem  43724  iuneq1i  45090  cbvmpo2  45102  cbvmpo1  45103  cbvrabv2w  45133  mptssid  45247  fprodabs2  45610  stoweidlem13  46028  wallispilem4  46083  fourierdlem94  46215  fourierdlem102  46223  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fourierdlem114  46235  41prothprmlem2  47605  2exp340mod341  47720  8exp8mod9  47723  nfermltl8rev  47729  stgr1  47928  cbvmpox2  48252  dmmpossx2  48253  zlmodzxzequa  48413  zlmodzxzequap  48416  resinsn  48772  dfswapf2  48967