Theorem 3eqtr4i 2767

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

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

This theorem is referenced by:  cbvrabv  3407  rabrab  3421  cbvrabw  3432  cbvrabwOLD  3433  cbvrab  3437  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbcow  3862  csbco  3863  cbvrabcsfw  3888  cbvrabcsf  3892  un4  4125  incom  4159  in13  4181  in31  4182  in4  4184  symdifcom  4204  indifcom  4233  indir  4236  undir  4237  indifdir  4245  difdif2  4246  notrab  4272  dfnul3  4287  dfif5  4494  rabsnifsb  4677  prcom  4687  tprot  4704  tpcoma  4705  tpcomb  4706  tpass  4707  qdassr  4709  pw0  4766  pwpw0  4767  pwsn  4854  cbviun  4988  cbviin  4989  cbviung  4990  cbviing  4991  cbviunv  4992  cbviinv  4993  iunrab  5006  iunin1  5025  iinuni  5051  cbvopab  5168  cbvopabv  5169  cbvopab1  5170  cbvopab1g  5171  cbvopab2  5172  cbvopab1s  5173  cbvopab1v  5174  cbvopab2v  5175  unopab  5176  cbvmptf  5196  cbvmptfg  5197  cbvmptv  5200  iunopab  5505  dfid4  5518  dfid2  5519  dfid3  5520  rabxp  5670  fconstmpt  5684  csbxp  5723  inxpOLD  5779  cnvco  5832  csbdm  5844  rnmpt  5904  csbres  5939  resundi  5950  resundir  5951  resindi  5952  resindir  5953  rescom  5959  resima  5972  imadmrn  6027  cnvimarndm  6040  cnvi  6097  cnvin  6100  rnun  6101  imaundi  6105  cnvxp  6113  imainrect  6137  csbrn  6159  imacnvcnv  6162  resdmres  6188  imadmres  6190  resdifdir  6193  mptpreima  6194  dfpred3  6268  predin  6283  predun  6284  preddif  6285  frpoind  6298  cbviotaw  6453  cbviotavw  6454  cbviota  6455  sb8iota  6457  resdif  6793  opabiotadm  6913  fndmin  6988  fninfp  7118  cbvriotaw  7322  cbvriotavw  7323  cbvriota  7326  riotarab  7355  dfoprab2  7414  cbvoprab1  7443  cbvoprab2  7444  cbvoprab12  7445  cbvoprab12v  7446  cbvoprab3  7447  cbvoprab3v  7448  cbvmpox  7449  cbvmpov  7451  resoprab  7474  caov32  7583  caov31  7585  caov4  7587  caovlem2  7592  uniuni  7705  zfrep6  7897  ofmres  7926  dfopab2  7994  dfxp3  8003  dmmpossx  8008  fmpox  8009  fsplit  8057  ovtpos  8181  tposco  8197  frrlem5  8230  tfrlem10  8316  o2p2e4  8466  0map0sn0  8821  mapsncnv  8829  cbvixp  8850  cbvixpv  8851  xpcomco  8993  sbthlem6  9018  ttrclresv  9624  frind  9660  cardf2  9853  alephcard  9978  alephfplem1  10012  xp2dju  10085  djuassen  10087  infdju1  10098  pwdju1  10099  ackbij1lem14  10140  compsscnv  10279  dffin1-5  10296  ituniiun  10330  axdc2lem  10356  axdc3lem4  10361  axcclem  10365  pwcfsdom  10492  dmaddpi  10799  dmmulpi  10800  adderpqlem  10863  addassnq  10867  mulcanenq  10869  addcmpblnr  10978  mulcmpblnrlem  10979  ltsrpr  10986  mulgt0sr  11014  sqgt0sr  11015  axi2m1  11068  negiso  12120  nummac  12650  decsubi  12668  9t11e99  12735  fztpval  13500  seqval  13933  sqrecii  14104  sqdivi  14106  binom2i  14133  4bc2eq6  14250  hashgval  14254  revs1  14686  cats1cat  14782  trclublem  14916  shftdm  14992  shftidt2  15002  cji  15080  cbvsum  15616  cbvsumv  15617  sumfc  15630  ackbijnn  15749  cbvprod  15834  cbvprodv  15835  prodeq1i  15837  prodfc  15866  fsumcube  15981  divalglem2  16320  nn0expgcd  16489  nn0gcdsq  16677  prmreclem2  16843  prmrec  16848  hashbc0  16931  dec5nprm  16992  dec2nprm  16993  gcdi  16999  decsplit  17008  1259lem1  17056  1259lem4  17059  4001lem1  17066  phlstr  17264  oduval  18209  oduleval  18210  odubas  18212  lubdm  18270  glbdm  18283  oppgid  19283  symgbas0  19316  gsumcom2  19902  ringidval  20116  oppr1  20284  dfrhm2  20408  rmodislmod  20879  cnfldsub  21350  cnflddiv  21353  cnflddivOLD  21354  dvdsrzring  21414  pjdm  21660  pjfval2  21662  opsrtoslem1  22008  restco  23106  ufprim  23851  tgioo3  24748  oprpiece1res1  24903  oprpiece1res2  24904  volfiniun  25502  vitalilem4  25566  cbvitg  25731  cbvitgv  25732  itgresr  25734  cbvditg  25809  plyid  26168  coeidp  26223  dgrid  26224  sincos3rdpi  26480  logblog  26756  ang180lem2  26774  1cubrlem  26805  asin1  26858  log2ublem2  26911  log2ublem3  26912  emcllem5  26964  lgsdir2lem5  27294  lgsquadlem3  27347  2lgslem1b  27357  2lgsoddprmlem3d  27378  noextend  27632  nosupbday  27671  nosupbnd1  27680  nosupbnd2  27682  noinfbday  27686  noinfbnd1  27695  dmscut  27779  madeval2  27821  negs0s  27995  negs1s  27996  1p1e2s  28374  cchhllem  28908  ax5seglem7  28957  vtxval0  29061  iedgval0  29062  finsumvtxdg2ssteplem1  29568  wwlksnfi  29928  1wlkdlem1  30161  ex-un  30448  ex-pw  30453  ex-cnv  30461  ex-co  30462  bafval  30628  vsfval  30657  cnnvba  30703  cnnvm  30706  ip2dii  30868  siilem1  30875  h2hcau  31003  hvsubsub4i  31083  hvnegdii  31086  normlem3  31136  normlem8  31141  norm-iii-i  31163  normpar2i  31180  polid2i  31181  chjassi  31510  chj4i  31547  h1de2i  31577  spanunsni  31603  fh3i  31647  fh4i  31648  qlax4i  31654  qlaxr3i  31660  3oalem5  31690  pjadjii  31698  pjsubii  31702  hoadd32i  31802  cnvadj  31916  hh0oi  31927  hhcno  31928  hhcnf  31929  nmopnegi  31989  lnophmlem2  32041  branmfn  32129  dmrab  32520  3unrab  32527  abrexexd  32533  cbviunf  32579  maprnin  32759  dpmul10  32925  dpexpp1  32938  dpadd3  32942  dpmul  32943  dpmul4  32944  psgnfzto1st  33136  cycpmconjs  33187  fracbas  33336  cos9thpiminplylem5  33892  lmlimxrge0  34054  zrhre  34125  qqhre  34126  rrhre  34127  cbvesum  34148  cbvesumv  34149  unibrsiga  34292  eulerpartlemt  34477  eulerpartgbij  34478  ballotlemrinv  34640  hgt750lem2  34758  bnj1146  34896  bnj893  35033  bnj1234  35118  r11  35199  r12  35200  subfacp1lem1  35322  kur14lem2  35350  kur14lem5  35353  kur14lem7  35355  cvmscld  35416  satfv1lem  35505  fmla0  35525  mvtval  35643  mthmpps  35725  fixun  36050  rabeqbii  36337  iuneq12i  36338  iineq1i  36339  iineq12i  36340  riotaeqbii  36341  ixpeq1i  36343  sumeq2si  36345  prodeq2si  36347  itgeq12i  36349  ditgeq123i  36352  cbvcsbvw2  36374  cbviunvw2  36375  cbviinvw2  36376  cbvmptvw2  36377  cbvriotavw2  36379  cbvoprab1vw  36380  cbvoprab2vw  36381  cbvoprab123vw  36382  cbvoprab23vw  36383  cbvoprab13vw  36384  cbvmpovw2  36385  cbvmpo1vw2  36386  cbvmpo2vw2  36387  cbvixpvw2  36388  cbvprodvw2  36390  cbvitgvw2  36391  cbvditgvw2  36392  bj-inrab  37071  bj-inrab3  37073  bj-gabeqis  37082  bj-pr1un  37147  bj-pr2un  37161  bj-dfid2ALT  37209  bj-mpomptALT  37263  rnmptsn  37479  f1omptsnlem  37480  rabiun  37733  phpreu  37744  poimirlem18  37778  ovoliunnfl  37802  voliunnfl  37804  mbfposadd  37807  asindmre  37843  abeqin  38389  rncnvepres  38441  qsresid  38463  dmxrn  38511  rnxrn  38545  xrnres  38549  xrnres2  38550  xrnres3  38551  dmxrncnvepres2  38557  dfsucmap3  38576  dfsucmap2  38577  rncossdmcoss  38657  1cosscnvxrn  38677  refrelsredund4  38828  mpets  39040  cdleme25cv  40557  sn-iotalemcor  42420  sqdeccom12  42486  sumcubes  42510  resuppsinopn  42560  sn-00idlem2  42596  sn-1ticom  42632  mendsca  43369  areaquad  43400  onsucrn  43455  df3o2  43497  df3o3  43498  omcl3g  43518  dfno2  43611  cnvrcl0  43808  sqrtcvallem1  43814  trclrelexplem  43894  iuneq1i  45271  cbvmpo2  45283  cbvmpo1  45284  cbvrabv2w  45314  mptssid  45427  fprodabs2  45783  stoweidlem13  46199  wallispilem4  46254  fourierdlem94  46386  fourierdlem102  46394  fourierdlem111  46403  fourierdlem112  46404  fourierdlem113  46405  fourierdlem114  46406  41prothprmlem2  47806  2exp340mod341  47921  8exp8mod9  47924  nfermltl8rev  47930  stgr1  48149  gpgprismgr4cycllem6  48288  gpgprismgr4cycllem9  48291  gpgprismgr4cycllem10  48292  cbvmpox2  48524  dmmpossx2  48525  zlmodzxzequa  48684  zlmodzxzequap  48687  resinsn  49059  dfswapf2  49448