Theorem 3eqtr4i 2770

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

Syntax hints:   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  cbvrabv  3400  cbvrabw  3425  cbvrabwOLD  3426  cbvrab  3429  cbvcsbw  3848  cbvcsb  3849  cbvcsbv  3850  csbcow  3853  csbco  3854  cbvrabcsfw  3879  cbvrabcsf  3883  un4  4116  incom  4150  in13  4172  in31  4173  in4  4175  symdifcom  4195  indifcom  4224  indir  4227  undir  4228  indifdir  4236  difdif2  4237  notrab  4263  dfnul3  4278  dfif5  4484  rabsnifsb  4667  prcom  4677  tprot  4694  tpcoma  4695  tpcomb  4696  tpass  4697  qdassr  4699  pw0  4756  pwpw0  4757  pwsn  4844  cbviun  4978  cbviin  4979  cbviung  4980  cbviing  4981  cbviunv  4982  cbviinv  4983  iunrab  4996  iunin1  5015  iinuni  5041  cbvopab  5158  cbvopabv  5159  cbvopab1  5160  cbvopab1g  5161  cbvopab2  5162  cbvopab1s  5163  cbvopab1v  5164  cbvopab2v  5165  unopab  5166  cbvmptf  5186  cbvmptfg  5187  cbvmptv  5190  iunopab  5508  dfid4  5521  dfid2  5522  dfid3  5523  rabxp  5673  fconstmpt  5687  csbxp  5726  inxpOLD  5782  cnvco  5835  csbdm  5847  rnmpt  5907  csbres  5942  resundi  5953  resundir  5954  resindi  5955  resindir  5956  rescom  5962  resima  5975  imadmrn  6030  cnvimarndm  6043  cnvi  6100  cnvin  6103  rnun  6104  imaundi  6108  cnvxp  6116  imainrect  6140  csbrn  6162  imacnvcnv  6165  resdmres  6191  imadmres  6193  resdifdir  6196  mptpreima  6197  dfpred3  6271  predin  6286  predun  6287  preddif  6288  frpoind  6301  cbviotaw  6456  cbviotavw  6457  cbviota  6458  sb8iota  6460  resdif  6796  opabiotadm  6916  fndmin  6992  fninfp  7123  cbvriotaw  7327  cbvriotavw  7328  cbvriota  7331  riotarab  7360  dfoprab2  7419  cbvoprab1  7448  cbvoprab2  7449  cbvoprab12  7450  cbvoprab12v  7451  cbvoprab3  7452  cbvoprab3v  7453  cbvmpox  7454  cbvmpov  7456  resoprab  7479  caov32  7588  caov31  7590  caov4  7592  caovlem2  7597  uniuni  7710  zfrep6OLD  7902  ofmres  7931  dfopab2  7999  dfxp3  8008  dmmpossx  8013  fmpox  8014  fsplit  8061  ovtpos  8185  tposco  8201  frrlem5  8234  tfrlem10  8320  o2p2e4  8470  0map0sn0  8827  mapsncnv  8835  cbvixp  8856  cbvixpv  8857  xpcomco  8999  sbthlem6  9024  ttrclresv  9632  frind  9668  cardf2  9861  alephcard  9986  alephfplem1  10020  xp2dju  10093  djuassen  10095  infdju1  10106  pwdju1  10107  ackbij1lem14  10148  compsscnv  10287  dffin1-5  10304  ituniiun  10338  axdc2lem  10364  axdc3lem4  10369  axcclem  10373  pwcfsdom  10500  dmaddpi  10807  dmmulpi  10808  adderpqlem  10871  addassnq  10875  mulcanenq  10877  addcmpblnr  10986  mulcmpblnrlem  10987  ltsrpr  10994  mulgt0sr  11022  sqgt0sr  11023  axi2m1  11076  negiso  12130  nummac  12683  decsubi  12701  9t11e99  12768  fztpval  13534  seqval  13968  sqrecii  14139  sqdivi  14141  binom2i  14168  4bc2eq6  14285  hashgval  14289  revs1  14721  cats1cat  14817  trclublem  14951  shftdm  15027  shftidt2  15037  cji  15115  cbvsum  15651  cbvsumv  15652  sumfc  15665  ackbijnn  15787  cbvprod  15872  cbvprodv  15873  prodeq1i  15875  prodfc  15904  fsumcube  16019  divalglem2  16358  nn0expgcd  16527  nn0gcdsq  16716  prmreclem2  16882  prmrec  16887  hashbc0  16970  dec5nprm  17031  dec2nprm  17032  gcdi  17038  decsplit  17047  1259lem1  17095  1259lem4  17098  4001lem1  17105  phlstr  17303  oduval  18248  oduleval  18249  odubas  18251  lubdm  18309  glbdm  18322  oppgid  19325  symgbas0  19358  gsumcom2  19944  ringidval  20158  oppr1  20324  dfrhm2  20448  rmodislmod  20919  cnfldsub  21390  cnflddiv  21393  cnflddivOLD  21394  dvdsrzring  21454  pjdm  21700  pjfval2  21702  opsrtoslem1  22046  restco  23142  ufprim  23887  tgioo3  24784  oprpiece1res1  24931  oprpiece1res2  24932  volfiniun  25527  vitalilem4  25591  cbvitg  25756  cbvitgv  25757  itgresr  25759  cbvditg  25834  plyid  26187  coeidp  26241  dgrid  26242  sincos3rdpi  26497  logblog  26772  ang180lem2  26790  1cubrlem  26821  asin1  26874  log2ublem2  26927  log2ublem3  26928  emcllem5  26980  lgsdir2lem5  27309  lgsquadlem3  27362  2lgslem1b  27372  2lgsoddprmlem3d  27393  noextend  27647  nosupbday  27686  nosupbnd1  27695  nosupbnd2  27697  noinfbday  27701  noinfbnd1  27710  dmcuts  27800  madeval2  27842  neg0s  28035  neg1s  28036  cchhllem  28972  ax5seglem7  29021  vtxval0  29125  iedgval0  29126  finsumvtxdg2ssteplem1  29632  wwlksnfi  29992  1wlkdlem1  30225  ex-un  30512  ex-pw  30517  ex-cnv  30525  ex-co  30526  bafval  30693  vsfval  30722  cnnvba  30768  cnnvm  30771  ip2dii  30933  siilem1  30940  h2hcau  31068  hvsubsub4i  31148  hvnegdii  31151  normlem3  31201  normlem8  31206  norm-iii-i  31228  normpar2i  31245  polid2i  31246  chjassi  31575  chj4i  31612  h1de2i  31642  spanunsni  31668  fh3i  31712  fh4i  31713  qlax4i  31719  qlaxr3i  31725  3oalem5  31755  pjadjii  31763  pjsubii  31767  hoadd32i  31867  cnvadj  31981  hh0oi  31992  hhcno  31993  hhcnf  31994  nmopnegi  32054  lnophmlem2  32106  branmfn  32194  dmrab  32584  3unrab  32591  abrexexd  32597  cbviunf  32643  maprnin  32822  dpmul10  32972  dpexpp1  32985  dpadd3  32989  dpmul  32990  dpmul4  32991  psgnfzto1st  33184  cycpmconjs  33235  fracbas  33384  cos9thpiminplylem5  33949  lmlimxrge0  34111  zrhre  34182  qqhre  34183  rrhre  34184  cbvesum  34205  cbvesumv  34206  unibrsiga  34349  eulerpartlemt  34534  eulerpartgbij  34535  ballotlemrinv  34697  hgt750lem2  34815  bnj1146  34952  bnj893  35089  bnj1234  35174  r11  35256  r12  35257  subfacp1lem1  35380  kur14lem2  35408  kur14lem5  35411  kur14lem7  35413  cvmscld  35474  satfv1lem  35563  fmla0  35583  mvtval  35701  mthmpps  35783  fixun  36108  rabeqbii  36395  iuneq12i  36396  iineq1i  36397  iineq12i  36398  riotaeqbii  36399  ixpeq1i  36401  sumeq2si  36403  prodeq2si  36405  itgeq12i  36407  ditgeq123i  36410  cbvcsbvw2  36432  cbviunvw2  36433  cbviinvw2  36434  cbvmptvw2  36435  cbvriotavw2  36437  cbvoprab1vw  36438  cbvoprab2vw  36439  cbvoprab123vw  36440  cbvoprab23vw  36441  cbvoprab13vw  36442  cbvmpovw2  36443  cbvmpo1vw2  36444  cbvmpo2vw2  36445  cbvixpvw2  36446  cbvprodvw2  36448  cbvitgvw2  36449  cbvditgvw2  36450  ttcun  36713  ttciun  36715  bj-inrab  37253  bj-inrab3  37255  bj-gabeqis  37264  bj-pr1un  37329  bj-pr2un  37343  bj-dfid2ALT  37391  bj-mpomptALT  37450  rnmptsn  37668  f1omptsnlem  37669  rabiun  37931  phpreu  37942  poimirlem18  37976  ovoliunnfl  38000  voliunnfl  38002  mbfposadd  38005  asindmre  38041  abeqin  38592  rncnvepres  38647  qsresid  38669  dmxrn  38725  rnxrn  38759  xrnres  38763  xrnres2  38764  xrnres3  38765  dmxrncnvepres2  38771  dfsucmap3  38801  dfsucmap2  38802  rncossdmcoss  38883  1cosscnvxrn  38903  refrelsredund4  39054  mpets  39294  dfpetparts2  39310  dfpeters2  39312  petseq  39314  pets2eq  39315  cdleme25cv  40821  sn-iotalemcor  42680  sqdeccom12  42738  sumcubes  42762  resuppsinopn  42812  sn-00idlem2  42848  sn-1ticom  42884  mendsca  43634  areaquad  43665  onsucrn  43720  df3o2  43762  df3o3  43763  omcl3g  43783  dfno2  43876  cnvrcl0  44073  sqrtcvallem1  44079  trclrelexplem  44159  iuneq1i  45536  cbvmpo2  45548  cbvmpo1  45549  cbvrabv2w  45579  mptssid  45691  fprodabs2  46046  stoweidlem13  46462  wallispilem4  46517  fourierdlem94  46649  fourierdlem102  46657  fourierdlem111  46666  fourierdlem112  46667  fourierdlem113  46668  fourierdlem114  46669  41prothprmlem2  48096  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  stgr1  48452  gpgprismgr4cycllem6  48591  gpgprismgr4cycllem9  48594  gpgprismgr4cycllem10  48595  cbvmpox2  48827  dmmpossx2  48828  zlmodzxzequa  48987  zlmodzxzequap  48990  resinsn  49362  dfswapf2  49751