Theorem 3eqtr4i 2764

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 2757	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2757	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 2121  ax-ext 2703

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

This theorem is referenced by:  cbvrabv  3405  rabrab  3419  cbvrabw  3430  cbvrabwOLD  3431  cbvrab  3435  cbvcsbw  3855  cbvcsb  3856  cbvcsbv  3857  csbcow  3860  csbco  3861  cbvrabcsfw  3886  cbvrabcsf  3890  un4  4122  incom  4156  in13  4178  in31  4179  in4  4181  symdifcom  4201  indifcom  4230  indir  4233  undir  4234  indifdir  4242  difdif2  4243  notrab  4269  dfnul3  4284  dfif5  4489  rabsnifsb  4672  prcom  4682  tprot  4699  tpcoma  4700  tpcomb  4701  tpass  4702  qdassr  4704  pw0  4761  pwpw0  4762  pwsn  4849  cbviun  4983  cbviin  4984  cbviung  4985  cbviing  4986  cbviunv  4987  cbviinv  4988  iunrab  4999  iunin1  5018  iinuni  5044  cbvopab  5161  cbvopabv  5162  cbvopab1  5163  cbvopab1g  5164  cbvopab2  5165  cbvopab1s  5166  cbvopab1v  5167  cbvopab2v  5168  unopab  5169  cbvmptf  5189  cbvmptfg  5190  cbvmptv  5193  iunopab  5497  dfid4  5510  dfid2  5511  dfid3  5512  rabxp  5662  fconstmpt  5676  csbxp  5715  inxpOLD  5771  cnvco  5824  csbdm  5836  rnmpt  5896  csbres  5930  resundi  5941  resundir  5942  resindi  5943  resindir  5944  rescom  5950  resima  5963  imadmrn  6018  cnvimarndm  6031  cnvi  6088  cnvin  6091  rnun  6092  imaundi  6096  cnvxp  6104  imainrect  6128  csbrn  6150  imacnvcnv  6153  resdmres  6179  imadmres  6181  resdifdir  6184  mptpreima  6185  dfpred3  6259  predin  6274  predun  6275  preddif  6276  frpoind  6289  cbviotaw  6444  cbviotavw  6445  cbviota  6446  sb8iota  6448  resdif  6784  opabiotadm  6903  fndmin  6978  fninfp  7108  cbvriotaw  7312  cbvriotavw  7313  cbvriota  7316  riotarab  7345  dfoprab2  7404  cbvoprab1  7433  cbvoprab2  7434  cbvoprab12  7435  cbvoprab12v  7436  cbvoprab3  7437  cbvoprab3v  7438  cbvmpox  7439  cbvmpov  7441  resoprab  7464  caov32  7573  caov31  7575  caov4  7577  caovlem2  7582  uniuni  7695  zfrep6  7887  ofmres  7916  dfopab2  7984  dfxp3  7993  dmmpossx  7998  fmpox  7999  fsplit  8047  ovtpos  8171  tposco  8187  frrlem5  8220  tfrlem10  8306  o2p2e4  8456  0map0sn0  8809  mapsncnv  8817  cbvixp  8838  cbvixpv  8839  xpcomco  8980  sbthlem6  9005  ttrclresv  9607  frind  9643  cardf2  9836  alephcard  9961  alephfplem1  9995  xp2dju  10068  djuassen  10070  infdju1  10081  pwdju1  10082  ackbij1lem14  10123  compsscnv  10262  dffin1-5  10279  ituniiun  10313  axdc2lem  10339  axdc3lem4  10344  axcclem  10348  pwcfsdom  10474  dmaddpi  10781  dmmulpi  10782  adderpqlem  10845  addassnq  10849  mulcanenq  10851  addcmpblnr  10960  mulcmpblnrlem  10961  ltsrpr  10968  mulgt0sr  10996  sqgt0sr  10997  axi2m1  11050  negiso  12102  nummac  12633  decsubi  12651  9t11e99  12718  fztpval  13486  seqval  13919  sqrecii  14090  sqdivi  14092  binom2i  14119  4bc2eq6  14236  hashgval  14240  revs1  14672  cats1cat  14768  trclublem  14902  shftdm  14978  shftidt2  14988  cji  15066  cbvsum  15602  cbvsumv  15603  sumfc  15616  ackbijnn  15735  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  prodfc  15852  fsumcube  15967  divalglem2  16306  nn0expgcd  16475  nn0gcdsq  16663  prmreclem2  16829  prmrec  16834  hashbc0  16917  dec5nprm  16978  dec2nprm  16979  gcdi  16985  decsplit  16994  1259lem1  17042  1259lem4  17045  4001lem1  17052  phlstr  17250  oduval  18194  oduleval  18195  odubas  18197  lubdm  18255  glbdm  18268  oppgid  19268  symgbas0  19301  gsumcom2  19887  ringidval  20101  oppr1  20268  dfrhm2  20392  rmodislmod  20863  cnfldsub  21334  cnflddiv  21337  cnflddivOLD  21338  dvdsrzring  21398  pjdm  21644  pjfval2  21646  opsrtoslem1  21990  restco  23079  ufprim  23824  tgioo3  24721  oprpiece1res1  24876  oprpiece1res2  24877  volfiniun  25475  vitalilem4  25539  cbvitg  25704  cbvitgv  25705  itgresr  25707  cbvditg  25782  plyid  26141  coeidp  26196  dgrid  26197  sincos3rdpi  26453  logblog  26729  ang180lem2  26747  1cubrlem  26778  asin1  26831  log2ublem2  26884  log2ublem3  26885  emcllem5  26937  lgsdir2lem5  27267  lgsquadlem3  27320  2lgslem1b  27330  2lgsoddprmlem3d  27351  noextend  27605  nosupbday  27644  nosupbnd1  27653  nosupbnd2  27655  noinfbday  27659  noinfbnd1  27668  dmscut  27752  madeval2  27794  negs0s  27968  negs1s  27969  1p1e2s  28339  cchhllem  28865  ax5seglem7  28913  vtxval0  29017  iedgval0  29018  finsumvtxdg2ssteplem1  29524  wwlksnfi  29884  1wlkdlem1  30117  ex-un  30404  ex-pw  30409  ex-cnv  30417  ex-co  30418  bafval  30584  vsfval  30613  cnnvba  30659  cnnvm  30662  ip2dii  30824  siilem1  30831  h2hcau  30959  hvsubsub4i  31039  hvnegdii  31042  normlem3  31092  normlem8  31097  norm-iii-i  31119  normpar2i  31136  polid2i  31137  chjassi  31466  chj4i  31503  h1de2i  31533  spanunsni  31559  fh3i  31603  fh4i  31604  qlax4i  31610  qlaxr3i  31616  3oalem5  31646  pjadjii  31654  pjsubii  31658  hoadd32i  31758  cnvadj  31872  hh0oi  31883  hhcno  31884  hhcnf  31885  nmopnegi  31945  lnophmlem2  31997  branmfn  32085  dmrab  32476  3unrab  32483  abrexexd  32489  cbviunf  32535  maprnin  32714  dpmul10  32875  dpexpp1  32888  dpadd3  32892  dpmul  32893  dpmul4  32894  psgnfzto1st  33074  cycpmconjs  33125  fracbas  33271  cos9thpiminplylem5  33799  lmlimxrge0  33961  zrhre  34032  qqhre  34033  rrhre  34034  cbvesum  34055  cbvesumv  34056  unibrsiga  34199  eulerpartlemt  34384  eulerpartgbij  34385  ballotlemrinv  34547  hgt750lem2  34665  bnj1146  34803  bnj893  34940  bnj1234  35025  r11  35105  r12  35106  subfacp1lem1  35223  kur14lem2  35251  kur14lem5  35254  kur14lem7  35256  cvmscld  35317  satfv1lem  35406  fmla0  35426  mvtval  35544  mthmpps  35626  fixun  35951  rabeqbii  36238  iuneq12i  36239  iineq1i  36240  iineq12i  36241  riotaeqbii  36242  ixpeq1i  36244  sumeq2si  36246  prodeq2si  36248  itgeq12i  36250  ditgeq123i  36253  cbvcsbvw2  36275  cbviunvw2  36276  cbviinvw2  36277  cbvmptvw2  36278  cbvriotavw2  36280  cbvoprab1vw  36281  cbvoprab2vw  36282  cbvoprab123vw  36283  cbvoprab23vw  36284  cbvoprab13vw  36285  cbvmpovw2  36286  cbvmpo1vw2  36287  cbvmpo2vw2  36288  cbvixpvw2  36289  cbvprodvw2  36291  cbvitgvw2  36292  cbvditgvw2  36293  bj-inrab  36971  bj-inrab3  36973  bj-gabeqis  36982  bj-pr1un  37047  bj-pr2un  37061  bj-dfid2ALT  37109  bj-mpomptALT  37163  rnmptsn  37379  f1omptsnlem  37380  rabiun  37643  phpreu  37654  poimirlem18  37688  ovoliunnfl  37712  voliunnfl  37714  mbfposadd  37717  asindmre  37753  abeqin  38299  rncnvepres  38351  qsresid  38373  dmxrn  38421  rnxrn  38455  xrnres  38459  xrnres2  38460  xrnres3  38461  dmxrncnvepres2  38467  dfsucmap3  38486  dfsucmap2  38487  rncossdmcoss  38567  1cosscnvxrn  38587  refrelsredund4  38738  mpets  38950  cdleme25cv  40467  sn-iotalemcor  42325  sqdeccom12  42392  sumcubes  42416  resuppsinopn  42466  sn-00idlem2  42502  sn-1ticom  42538  mendsca  43288  areaquad  43319  onsucrn  43374  df3o2  43416  df3o3  43417  omcl3g  43437  dfno2  43531  cnvrcl0  43728  sqrtcvallem1  43734  trclrelexplem  43814  iuneq1i  45192  cbvmpo2  45204  cbvmpo1  45205  cbvrabv2w  45235  mptssid  45348  fprodabs2  45705  stoweidlem13  46121  wallispilem4  46176  fourierdlem94  46308  fourierdlem102  46316  fourierdlem111  46325  fourierdlem112  46326  fourierdlem113  46327  fourierdlem114  46328  41prothprmlem2  47728  2exp340mod341  47843  8exp8mod9  47846  nfermltl8rev  47852  stgr1  48071  gpgprismgr4cycllem6  48210  gpgprismgr4cycllem9  48213  gpgprismgr4cycllem10  48214  cbvmpox2  48446  dmmpossx2  48447  zlmodzxzequa  48607  zlmodzxzequap  48610  resinsn  48982  dfswapf2  49372