Theorem 3eqtr4i 2769

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

Syntax hints:   = wceq 1541

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  cbvrabv  3409  rabrab  3423  cbvrabw  3434  cbvrabwOLD  3435  cbvrab  3439  cbvcsbw  3859  cbvcsb  3860  cbvcsbv  3861  csbcow  3864  csbco  3865  cbvrabcsfw  3890  cbvrabcsf  3894  un4  4127  incom  4161  in13  4183  in31  4184  in4  4186  symdifcom  4206  indifcom  4235  indir  4238  undir  4239  indifdir  4247  difdif2  4248  notrab  4274  dfnul3  4289  dfif5  4496  rabsnifsb  4679  prcom  4689  tprot  4706  tpcoma  4707  tpcomb  4708  tpass  4709  qdassr  4711  pw0  4768  pwpw0  4769  pwsn  4856  cbviun  4990  cbviin  4991  cbviung  4992  cbviing  4993  cbviunv  4994  cbviinv  4995  iunrab  5008  iunin1  5027  iinuni  5053  cbvopab  5170  cbvopabv  5171  cbvopab1  5172  cbvopab1g  5173  cbvopab2  5174  cbvopab1s  5175  cbvopab1v  5176  cbvopab2v  5177  unopab  5178  cbvmptf  5198  cbvmptfg  5199  cbvmptv  5202  iunopab  5507  dfid4  5520  dfid2  5521  dfid3  5522  rabxp  5672  fconstmpt  5686  csbxp  5725  inxpOLD  5781  cnvco  5834  csbdm  5846  rnmpt  5906  csbres  5941  resundi  5952  resundir  5953  resindi  5954  resindir  5955  rescom  5961  resima  5974  imadmrn  6029  cnvimarndm  6042  cnvi  6099  cnvin  6102  rnun  6103  imaundi  6107  cnvxp  6115  imainrect  6139  csbrn  6161  imacnvcnv  6164  resdmres  6190  imadmres  6192  resdifdir  6195  mptpreima  6196  dfpred3  6270  predin  6285  predun  6286  preddif  6287  frpoind  6300  cbviotaw  6455  cbviotavw  6456  cbviota  6457  sb8iota  6459  resdif  6795  opabiotadm  6915  fndmin  6990  fninfp  7120  cbvriotaw  7324  cbvriotavw  7325  cbvriota  7328  riotarab  7357  dfoprab2  7416  cbvoprab1  7445  cbvoprab2  7446  cbvoprab12  7447  cbvoprab12v  7448  cbvoprab3  7449  cbvoprab3v  7450  cbvmpox  7451  cbvmpov  7453  resoprab  7476  caov32  7585  caov31  7587  caov4  7589  caovlem2  7594  uniuni  7707  zfrep6  7899  ofmres  7928  dfopab2  7996  dfxp3  8005  dmmpossx  8010  fmpox  8011  fsplit  8059  ovtpos  8183  tposco  8199  frrlem5  8232  tfrlem10  8318  o2p2e4  8468  0map0sn0  8823  mapsncnv  8831  cbvixp  8852  cbvixpv  8853  xpcomco  8995  sbthlem6  9020  ttrclresv  9626  frind  9662  cardf2  9855  alephcard  9980  alephfplem1  10014  xp2dju  10087  djuassen  10089  infdju1  10100  pwdju1  10101  ackbij1lem14  10142  compsscnv  10281  dffin1-5  10298  ituniiun  10332  axdc2lem  10358  axdc3lem4  10363  axcclem  10367  pwcfsdom  10494  dmaddpi  10801  dmmulpi  10802  adderpqlem  10865  addassnq  10869  mulcanenq  10871  addcmpblnr  10980  mulcmpblnrlem  10981  ltsrpr  10988  mulgt0sr  11016  sqgt0sr  11017  axi2m1  11070  negiso  12122  nummac  12652  decsubi  12670  9t11e99  12737  fztpval  13502  seqval  13935  sqrecii  14106  sqdivi  14108  binom2i  14135  4bc2eq6  14252  hashgval  14256  revs1  14688  cats1cat  14784  trclublem  14918  shftdm  14994  shftidt2  15004  cji  15082  cbvsum  15618  cbvsumv  15619  sumfc  15632  ackbijnn  15751  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  prodfc  15868  fsumcube  15983  divalglem2  16322  nn0expgcd  16491  nn0gcdsq  16679  prmreclem2  16845  prmrec  16850  hashbc0  16933  dec5nprm  16994  dec2nprm  16995  gcdi  17001  decsplit  17010  1259lem1  17058  1259lem4  17061  4001lem1  17068  phlstr  17266  oduval  18211  oduleval  18212  odubas  18214  lubdm  18272  glbdm  18285  oppgid  19285  symgbas0  19318  gsumcom2  19904  ringidval  20118  oppr1  20286  dfrhm2  20410  rmodislmod  20881  cnfldsub  21352  cnflddiv  21355  cnflddivOLD  21356  dvdsrzring  21416  pjdm  21662  pjfval2  21664  opsrtoslem1  22010  restco  23108  ufprim  23853  tgioo3  24750  oprpiece1res1  24905  oprpiece1res2  24906  volfiniun  25504  vitalilem4  25568  cbvitg  25733  cbvitgv  25734  itgresr  25736  cbvditg  25811  plyid  26170  coeidp  26225  dgrid  26226  sincos3rdpi  26482  logblog  26758  ang180lem2  26776  1cubrlem  26807  asin1  26860  log2ublem2  26913  log2ublem3  26914  emcllem5  26966  lgsdir2lem5  27296  lgsquadlem3  27349  2lgslem1b  27359  2lgsoddprmlem3d  27380  noextend  27634  nosupbday  27673  nosupbnd1  27682  nosupbnd2  27684  noinfbday  27688  noinfbnd1  27697  dmcuts  27787  madeval2  27829  neg0s  28022  neg1s  28023  cchhllem  28959  ax5seglem7  29008  vtxval0  29112  iedgval0  29113  finsumvtxdg2ssteplem1  29619  wwlksnfi  29979  1wlkdlem1  30212  ex-un  30499  ex-pw  30504  ex-cnv  30512  ex-co  30513  bafval  30679  vsfval  30708  cnnvba  30754  cnnvm  30757  ip2dii  30919  siilem1  30926  h2hcau  31054  hvsubsub4i  31134  hvnegdii  31137  normlem3  31187  normlem8  31192  norm-iii-i  31214  normpar2i  31231  polid2i  31232  chjassi  31561  chj4i  31598  h1de2i  31628  spanunsni  31654  fh3i  31698  fh4i  31699  qlax4i  31705  qlaxr3i  31711  3oalem5  31741  pjadjii  31749  pjsubii  31753  hoadd32i  31853  cnvadj  31967  hh0oi  31978  hhcno  31979  hhcnf  31980  nmopnegi  32040  lnophmlem2  32092  branmfn  32180  dmrab  32571  3unrab  32578  abrexexd  32584  cbviunf  32630  maprnin  32810  dpmul10  32976  dpexpp1  32989  dpadd3  32993  dpmul  32994  dpmul4  32995  psgnfzto1st  33187  cycpmconjs  33238  fracbas  33387  cos9thpiminplylem5  33943  lmlimxrge0  34105  zrhre  34176  qqhre  34177  rrhre  34178  cbvesum  34199  cbvesumv  34200  unibrsiga  34343  eulerpartlemt  34528  eulerpartgbij  34529  ballotlemrinv  34691  hgt750lem2  34809  bnj1146  34947  bnj893  35084  bnj1234  35169  r11  35250  r12  35251  subfacp1lem1  35373  kur14lem2  35401  kur14lem5  35404  kur14lem7  35406  cvmscld  35467  satfv1lem  35556  fmla0  35576  mvtval  35694  mthmpps  35776  fixun  36101  rabeqbii  36388  iuneq12i  36389  iineq1i  36390  iineq12i  36391  riotaeqbii  36392  ixpeq1i  36394  sumeq2si  36396  prodeq2si  36398  itgeq12i  36400  ditgeq123i  36403  cbvcsbvw2  36425  cbviunvw2  36426  cbviinvw2  36427  cbvmptvw2  36428  cbvriotavw2  36430  cbvoprab1vw  36431  cbvoprab2vw  36432  cbvoprab123vw  36433  cbvoprab23vw  36434  cbvoprab13vw  36435  cbvmpovw2  36436  cbvmpo1vw2  36437  cbvmpo2vw2  36438  cbvixpvw2  36439  cbvprodvw2  36441  cbvitgvw2  36442  cbvditgvw2  36443  bj-inrab  37128  bj-inrab3  37130  bj-gabeqis  37139  bj-pr1un  37204  bj-pr2un  37218  bj-dfid2ALT  37266  bj-mpomptALT  37324  rnmptsn  37540  f1omptsnlem  37541  rabiun  37794  phpreu  37805  poimirlem18  37839  ovoliunnfl  37863  voliunnfl  37865  mbfposadd  37868  asindmre  37904  abeqin  38450  rncnvepres  38504  qsresid  38526  dmxrn  38582  rnxrn  38616  xrnres  38620  xrnres2  38621  xrnres3  38622  dmxrncnvepres2  38628  dfsucmap3  38647  dfsucmap2  38648  rncossdmcoss  38728  1cosscnvxrn  38748  refrelsredund4  38899  mpets  39111  cdleme25cv  40628  sn-iotalemcor  42488  sqdeccom12  42554  sumcubes  42578  resuppsinopn  42628  sn-00idlem2  42664  sn-1ticom  42700  mendsca  43437  areaquad  43468  onsucrn  43523  df3o2  43565  df3o3  43566  omcl3g  43586  dfno2  43679  cnvrcl0  43876  sqrtcvallem1  43882  trclrelexplem  43962  iuneq1i  45339  cbvmpo2  45351  cbvmpo1  45352  cbvrabv2w  45382  mptssid  45495  fprodabs2  45851  stoweidlem13  46267  wallispilem4  46322  fourierdlem94  46454  fourierdlem102  46462  fourierdlem111  46471  fourierdlem112  46472  fourierdlem113  46473  fourierdlem114  46474  41prothprmlem2  47874  2exp340mod341  47989  8exp8mod9  47992  nfermltl8rev  47998  stgr1  48217  gpgprismgr4cycllem6  48356  gpgprismgr4cycllem9  48359  gpgprismgr4cycllem10  48360  cbvmpox2  48592  dmmpossx2  48593  zlmodzxzequa  48752  zlmodzxzequap  48755  resinsn  49127  dfswapf2  49516