Theorem 3eqtr4i 2762

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 2755	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2755	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rabbiiaOLD  3410  cbvrabv  3416  rabrab  3430  cbvrabw  3441  cbvrabwOLD  3442  cbvrab  3446  cbvcsbw  3872  cbvcsb  3873  cbvcsbv  3874  csbcow  3877  csbco  3878  cbvrabcsfw  3903  cbvrabcsf  3907  un4  4138  incom  4172  in13  4194  in31  4195  in4  4197  symdifcom  4217  indifcom  4246  indir  4249  undir  4250  indifdir  4258  difdif2  4259  notrab  4285  dfnul3  4300  dfif5  4505  rabsnifsb  4686  prcom  4696  tprot  4713  tpcoma  4714  tpcomb  4715  tpass  4716  qdassr  4718  pw0  4776  pwpw0  4777  pwsn  4864  cbviun  5000  cbviin  5001  cbviung  5002  cbviing  5003  cbviunv  5004  cbviinv  5005  iunrab  5016  iunin1  5036  iinuni  5062  cbvopab  5179  cbvopabv  5180  cbvopab1  5181  cbvopab1g  5182  cbvopab2  5183  cbvopab1s  5184  cbvopab1v  5185  cbvopab2v  5186  unopab  5187  cbvmptf  5207  cbvmptfg  5208  cbvmptv  5211  iunopab  5519  iunopabOLD  5520  dfid4  5534  dfid2  5535  dfid3  5536  rabxp  5686  fconstmpt  5700  csbxp  5738  inxpOLD  5796  cnvco  5849  csbdm  5861  rnmpt  5921  csbres  5953  resundi  5964  resundir  5965  resindi  5966  resindir  5967  rescom  5973  resima  5986  imadmrn  6041  cnvimarndm  6054  cnvi  6114  cnvin  6117  rnun  6118  imaundi  6122  cnvxp  6130  imainrect  6154  csbrn  6176  imacnvcnv  6179  resdmres  6205  imadmres  6207  resdifdir  6210  mptpreima  6211  dfpred3  6285  predin  6300  predun  6301  preddif  6302  frpoind  6315  cbviotaw  6471  cbviotavw  6472  cbviota  6473  sb8iota  6475  resdif  6821  opabiotadm  6942  fndmin  7017  fninfp  7148  cbvriotaw  7353  cbvriotavw  7354  cbvriota  7357  riotarab  7386  dfoprab2  7447  cbvoprab1  7476  cbvoprab2  7477  cbvoprab12  7478  cbvoprab12v  7479  cbvoprab3  7480  cbvoprab3v  7481  cbvmpox  7482  cbvmpov  7484  resoprab  7507  caov32  7616  caov31  7618  caov4  7620  caovlem2  7625  uniuni  7738  zfrep6  7933  ofmres  7963  dfopab2  8031  dfxp3  8040  dmmpossx  8045  fmpox  8046  fsplit  8096  ovtpos  8220  tposco  8236  frrlem5  8269  tfrlem10  8355  o2p2e4  8505  0map0sn0  8858  mapsncnv  8866  cbvixp  8887  cbvixpv  8888  xpcomco  9031  sbthlem6  9056  1sdomOLD  9196  ttrclresv  9670  frind  9703  cardf2  9896  alephcard  10023  alephfplem1  10057  xp2dju  10130  djuassen  10132  infdju1  10143  pwdju1  10144  ackbij1lem14  10185  compsscnv  10324  dffin1-5  10341  ituniiun  10375  axdc2lem  10401  axdc3lem4  10406  axcclem  10410  pwcfsdom  10536  dmaddpi  10843  dmmulpi  10844  adderpqlem  10907  addassnq  10911  mulcanenq  10913  addcmpblnr  11022  mulcmpblnrlem  11023  ltsrpr  11030  mulgt0sr  11058  sqgt0sr  11059  axi2m1  11112  negiso  12163  nummac  12694  decsubi  12712  9t11e99  12779  fztpval  13547  seqval  13977  sqrecii  14148  sqdivi  14150  binom2i  14177  4bc2eq6  14294  hashgval  14298  revs1  14730  cats1cat  14827  trclublem  14961  shftdm  15037  shftidt2  15047  cji  15125  cbvsum  15661  cbvsumv  15662  sumfc  15675  ackbijnn  15794  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  prodfc  15911  fsumcube  16026  divalglem2  16365  nn0expgcd  16534  nn0gcdsq  16722  prmreclem2  16888  prmrec  16893  hashbc0  16976  dec5nprm  17037  dec2nprm  17038  gcdi  17044  decsplit  17053  1259lem1  17101  1259lem4  17104  4001lem1  17111  phlstr  17309  oduval  18249  oduleval  18250  odubas  18252  lubdm  18310  glbdm  18323  oppgid  19288  symgbas0  19319  gsumcom2  19905  ringidval  20092  oppr1  20259  dfrhm2  20383  rmodislmod  20836  cnfldsub  21309  cnflddiv  21312  cnflddivOLD  21313  dvdsrzring  21371  pjdm  21616  pjfval2  21618  opsrtoslem1  21962  restco  23051  ufprim  23796  tgioo3  24694  oprpiece1res1  24849  oprpiece1res2  24850  volfiniun  25448  vitalilem4  25512  cbvitg  25677  cbvitgv  25678  itgresr  25680  cbvditg  25755  plyid  26114  coeidp  26169  dgrid  26170  sincos3rdpi  26426  logblog  26702  ang180lem2  26720  1cubrlem  26751  asin1  26804  log2ublem2  26857  log2ublem3  26858  emcllem5  26910  lgsdir2lem5  27240  lgsquadlem3  27293  2lgslem1b  27303  2lgsoddprmlem3d  27324  noextend  27578  nosupbday  27617  nosupbnd1  27626  nosupbnd2  27628  noinfbday  27632  noinfbnd1  27641  dmscut  27723  madeval2  27761  negs0s  27932  negs1s  27933  1p1e2s  28302  cchhllem  28814  ax5seglem7  28862  vtxval0  28966  iedgval0  28967  finsumvtxdg2ssteplem1  29473  wwlksnfi  29836  1wlkdlem1  30066  ex-un  30353  ex-pw  30358  ex-cnv  30366  ex-co  30367  bafval  30533  vsfval  30562  cnnvba  30608  cnnvm  30611  ip2dii  30773  siilem1  30780  h2hcau  30908  hvsubsub4i  30988  hvnegdii  30991  normlem3  31041  normlem8  31046  norm-iii-i  31068  normpar2i  31085  polid2i  31086  chjassi  31415  chj4i  31452  h1de2i  31482  spanunsni  31508  fh3i  31552  fh4i  31553  qlax4i  31559  qlaxr3i  31565  3oalem5  31595  pjadjii  31603  pjsubii  31607  hoadd32i  31707  cnvadj  31821  hh0oi  31832  hhcno  31833  hhcnf  31834  nmopnegi  31894  lnophmlem2  31946  branmfn  32034  dmrab  32426  3unrab  32432  abrexexd  32438  cbviunf  32484  maprnin  32654  dpmul10  32815  dpexpp1  32828  dpadd3  32832  dpmul  32833  dpmul4  32834  psgnfzto1st  33062  cycpmconjs  33113  fracbas  33255  cos9thpiminplylem5  33776  lmlimxrge0  33938  zrhre  34009  qqhre  34010  rrhre  34011  cbvesum  34032  cbvesumv  34033  unibrsiga  34176  eulerpartlemt  34362  eulerpartgbij  34363  ballotlemrinv  34525  hgt750lem2  34643  bnj1146  34781  bnj893  34918  bnj1234  35003  subfacp1lem1  35166  kur14lem2  35194  kur14lem5  35197  kur14lem7  35199  cvmscld  35260  satfv1lem  35349  fmla0  35369  mvtval  35487  mthmpps  35569  fixun  35897  rabeqbii  36182  iuneq12i  36183  iineq1i  36184  iineq12i  36185  riotaeqbii  36186  ixpeq1i  36188  sumeq2si  36190  prodeq2si  36192  itgeq12i  36194  ditgeq123i  36197  cbvcsbvw2  36219  cbviunvw2  36220  cbviinvw2  36221  cbvmptvw2  36222  cbvriotavw2  36224  cbvoprab1vw  36225  cbvoprab2vw  36226  cbvoprab123vw  36227  cbvoprab23vw  36228  cbvoprab13vw  36229  cbvmpovw2  36230  cbvmpo1vw2  36231  cbvmpo2vw2  36232  cbvixpvw2  36233  cbvprodvw2  36235  cbvitgvw2  36236  cbvditgvw2  36237  bj-inrab  36915  bj-inrab3  36917  bj-gabeqis  36926  bj-pr1un  36991  bj-pr2un  37005  bj-dfid2ALT  37053  bj-mpomptALT  37107  rnmptsn  37323  f1omptsnlem  37324  rabiun  37587  phpreu  37598  poimirlem18  37632  ovoliunnfl  37656  voliunnfl  37658  mbfposadd  37661  asindmre  37697  abeqin  38241  rncnvepres  38291  qsresid  38313  dmxrn  38360  rnxrn  38384  xrnres  38388  xrnres2  38389  xrnres3  38390  rncossdmcoss  38446  1cosscnvxrn  38466  refrelsredund4  38623  mpets  38834  cdleme25cv  40352  sn-iotalemcor  42210  sqdeccom12  42277  sumcubes  42301  resuppsinopn  42351  sn-00idlem2  42387  sn-1ticom  42423  mendsca  43174  areaquad  43205  onsucrn  43260  df3o2  43302  df3o3  43303  omcl3g  43323  dfno2  43417  cnvrcl0  43614  sqrtcvallem1  43620  trclrelexplem  43700  iuneq1i  45079  cbvmpo2  45091  cbvmpo1  45092  cbvrabv2w  45122  mptssid  45235  fprodabs2  45593  stoweidlem13  46011  wallispilem4  46066  fourierdlem94  46198  fourierdlem102  46206  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fourierdlem114  46218  41prothprmlem2  47619  2exp340mod341  47734  8exp8mod9  47737  nfermltl8rev  47743  stgr1  47960  gpgprismgr4cycllem6  48090  gpgprismgr4cycllem9  48093  gpgprismgr4cycllem10  48094  cbvmpox2  48324  dmmpossx2  48325  zlmodzxzequa  48485  zlmodzxzequap  48488  resinsn  48860  dfswapf2  49250