Theorem 3eqtr4i 2768

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

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

This theorem is referenced by:  rabbiiaOLD  3420  cbvrabv  3426  rabrab  3440  cbvrabw  3452  cbvrabwOLD  3453  cbvrab  3458  cbvcsbw  3884  cbvcsb  3885  cbvcsbv  3886  csbcow  3889  csbco  3890  cbvrabcsfw  3915  cbvrabcsf  3919  un4  4150  incom  4184  in13  4206  in31  4207  in4  4209  symdifcom  4229  indifcom  4258  indir  4261  undir  4262  indifdir  4270  difdif2  4271  notrab  4297  dfnul3  4312  dfif5  4517  rabsnifsb  4698  prcom  4708  tprot  4725  tpcoma  4726  tpcomb  4727  tpass  4728  qdassr  4730  pw0  4788  pwpw0  4789  pwsn  4876  cbviun  5012  cbviin  5013  cbviung  5014  cbviing  5015  cbviunv  5016  cbviinv  5017  iunrab  5028  iunin1  5048  iinuni  5074  cbvopab  5191  cbvopabv  5192  cbvopab1  5193  cbvopab1g  5194  cbvopab2  5195  cbvopab1s  5196  cbvopab1v  5197  cbvopab2v  5199  unopab  5200  cbvmptf  5221  cbvmptfg  5222  cbvmptv  5225  iunopab  5534  iunopabOLD  5535  dfid4  5549  dfid2  5550  dfid3  5551  rabxp  5702  fconstmpt  5716  csbxp  5754  inxpOLD  5812  cnvco  5865  csbdm  5877  rnmpt  5937  csbres  5969  resundi  5980  resundir  5981  resindi  5982  resindir  5983  rescom  5989  resima  6002  imadmrn  6057  cnvimarndm  6070  cnvi  6130  cnvin  6133  rnun  6134  imaundi  6138  cnvxp  6146  imainrect  6170  csbrn  6192  imacnvcnv  6195  resdmres  6221  imadmres  6223  resdifdir  6226  mptpreima  6227  dfpred3  6301  predin  6316  predun  6317  preddif  6318  frpoind  6331  wfiOLD  6340  cbviotaw  6491  cbviotavw  6492  cbviota  6493  sb8iota  6495  resdif  6839  opabiotadm  6960  fndmin  7035  fninfp  7166  cbvriotaw  7371  cbvriotavw  7372  cbvriota  7375  riotarab  7404  dfoprab2  7465  cbvoprab1  7494  cbvoprab2  7495  cbvoprab12  7496  cbvoprab12v  7497  cbvoprab3  7498  cbvoprab3v  7499  cbvmpox  7500  cbvmpov  7502  resoprab  7525  caov32  7634  caov31  7636  caov4  7638  caovlem2  7643  uniuni  7756  zfrep6  7953  ofmres  7983  dfopab2  8051  dfxp3  8060  dmmpossx  8065  fmpox  8066  fsplit  8116  ovtpos  8240  tposco  8256  frrlem5  8289  tfrlem10  8401  o2p2e4  8553  0map0sn0  8899  mapsncnv  8907  cbvixp  8928  cbvixpv  8929  xpcomco  9076  sbthlem6  9102  1sdomOLD  9257  ttrclresv  9731  frind  9764  cardf2  9957  alephcard  10084  alephfplem1  10118  xp2dju  10191  djuassen  10193  infdju1  10204  pwdju1  10205  ackbij1lem14  10246  compsscnv  10385  dffin1-5  10402  ituniiun  10436  axdc2lem  10462  axdc3lem4  10467  axcclem  10471  pwcfsdom  10597  dmaddpi  10904  dmmulpi  10905  adderpqlem  10968  addassnq  10972  mulcanenq  10974  addcmpblnr  11083  mulcmpblnrlem  11084  ltsrpr  11091  mulgt0sr  11119  sqgt0sr  11120  axi2m1  11173  negiso  12222  nummac  12753  decsubi  12771  9t11e99  12838  fztpval  13603  seqval  14030  sqrecii  14201  sqdivi  14203  binom2i  14230  4bc2eq6  14347  hashgval  14351  revs1  14783  cats1cat  14880  trclublem  15014  shftdm  15090  shftidt2  15100  cji  15178  cbvsum  15711  cbvsumv  15712  sumfc  15725  ackbijnn  15844  cbvprod  15929  cbvprodv  15930  prodeq1i  15932  prodfc  15961  fsumcube  16076  divalglem2  16414  nn0expgcd  16583  nn0gcdsq  16771  prmreclem2  16937  prmrec  16942  hashbc0  17025  dec5nprm  17086  dec2nprm  17087  gcdi  17093  decsplit  17102  1259lem1  17150  1259lem4  17153  4001lem1  17160  phlstr  17360  oduval  18300  oduleval  18301  odubas  18303  lubdm  18361  glbdm  18374  oppgid  19339  symgbas0  19370  gsumcom2  19956  ringidval  20143  oppr1  20310  dfrhm2  20434  rmodislmod  20887  cnfldsub  21360  cnflddiv  21363  cnflddivOLD  21364  dvdsrzring  21422  pjdm  21667  pjfval2  21669  opsrtoslem1  22013  restco  23102  ufprim  23847  tgioo3  24745  oprpiece1res1  24900  oprpiece1res2  24901  volfiniun  25500  vitalilem4  25564  cbvitg  25729  cbvitgv  25730  itgresr  25732  cbvditg  25807  plyid  26166  coeidp  26221  dgrid  26222  sincos3rdpi  26478  logblog  26754  ang180lem2  26772  1cubrlem  26803  asin1  26856  log2ublem2  26909  log2ublem3  26910  emcllem5  26962  lgsdir2lem5  27292  lgsquadlem3  27345  2lgslem1b  27355  2lgsoddprmlem3d  27376  noextend  27630  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfbday  27684  noinfbnd1  27693  dmscut  27775  madeval2  27813  negs0s  27984  negs1s  27985  1p1e2s  28354  cchhllem  28866  ax5seglem7  28914  vtxval0  29018  iedgval0  29019  finsumvtxdg2ssteplem1  29525  wwlksnfi  29888  1wlkdlem1  30118  ex-un  30405  ex-pw  30410  ex-cnv  30418  ex-co  30419  bafval  30585  vsfval  30614  cnnvba  30660  cnnvm  30663  ip2dii  30825  siilem1  30832  h2hcau  30960  hvsubsub4i  31040  hvnegdii  31043  normlem3  31093  normlem8  31098  norm-iii-i  31120  normpar2i  31137  polid2i  31138  chjassi  31467  chj4i  31504  h1de2i  31534  spanunsni  31560  fh3i  31604  fh4i  31605  qlax4i  31611  qlaxr3i  31617  3oalem5  31647  pjadjii  31655  pjsubii  31659  hoadd32i  31759  cnvadj  31873  hh0oi  31884  hhcno  31885  hhcnf  31886  nmopnegi  31946  lnophmlem2  31998  branmfn  32086  dmrab  32478  3unrab  32484  abrexexd  32490  cbviunf  32536  maprnin  32708  dpmul10  32869  dpexpp1  32882  dpadd3  32886  dpmul  32887  dpmul4  32888  psgnfzto1st  33116  cycpmconjs  33167  fracbas  33299  cos9thpiminplylem5  33820  lmlimxrge0  33979  zrhre  34050  qqhre  34051  rrhre  34052  cbvesum  34073  cbvesumv  34074  unibrsiga  34217  eulerpartlemt  34403  eulerpartgbij  34404  ballotlemrinv  34566  hgt750lem2  34684  bnj1146  34822  bnj893  34959  bnj1234  35044  subfacp1lem1  35201  kur14lem2  35229  kur14lem5  35232  kur14lem7  35234  cvmscld  35295  satfv1lem  35384  fmla0  35404  mvtval  35522  mthmpps  35604  fixun  35927  rabeqbii  36212  iuneq12i  36213  iineq1i  36214  iineq12i  36215  riotaeqbii  36216  ixpeq1i  36218  sumeq2si  36220  prodeq2si  36222  itgeq12i  36224  ditgeq123i  36227  cbvcsbvw2  36249  cbviunvw2  36250  cbviinvw2  36251  cbvmptvw2  36252  cbvriotavw2  36254  cbvoprab1vw  36255  cbvoprab2vw  36256  cbvoprab123vw  36257  cbvoprab23vw  36258  cbvoprab13vw  36259  cbvmpovw2  36260  cbvmpo1vw2  36261  cbvmpo2vw2  36262  cbvixpvw2  36263  cbvprodvw2  36265  cbvitgvw2  36266  cbvditgvw2  36267  bj-inrab  36945  bj-inrab3  36947  bj-gabeqis  36956  bj-pr1un  37021  bj-pr2un  37035  bj-dfid2ALT  37083  bj-mpomptALT  37137  rnmptsn  37353  f1omptsnlem  37354  rabiun  37617  phpreu  37628  poimirlem18  37662  ovoliunnfl  37686  voliunnfl  37688  mbfposadd  37691  asindmre  37727  abeqin  38270  rncnvepres  38321  qsresid  38343  rnxrn  38416  xrnres  38420  xrnres2  38421  xrnres3  38422  rncossdmcoss  38473  1cosscnvxrn  38493  refrelsredund4  38650  mpets  38860  cdleme25cv  40377  sn-iotalemcor  42273  sqdeccom12  42339  sumcubes  42362  resuppsinopn  42406  sn-00idlem2  42442  sn-1ticom  42477  mendsca  43209  areaquad  43240  onsucrn  43295  df3o2  43337  df3o3  43338  omcl3g  43358  dfno2  43452  cnvrcl0  43649  sqrtcvallem1  43655  trclrelexplem  43735  iuneq1i  45109  cbvmpo2  45121  cbvmpo1  45122  cbvrabv2w  45152  mptssid  45265  fprodabs2  45624  stoweidlem13  46042  wallispilem4  46097  fourierdlem94  46229  fourierdlem102  46237  fourierdlem111  46246  fourierdlem112  46247  fourierdlem113  46248  fourierdlem114  46249  41prothprmlem2  47632  2exp340mod341  47747  8exp8mod9  47750  nfermltl8rev  47756  stgr1  47973  gpgprismgr4cycllem6  48099  gpgprismgr4cycllem9  48102  gpgprismgr4cycllem10  48103  cbvmpox2  48311  dmmpossx2  48312  zlmodzxzequa  48472  zlmodzxzequap  48475  resinsn  48847  dfswapf2  49178