Theorem 3eqtr4i 2769

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 2762	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2762	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

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

This theorem is referenced by:  rabbiiaOLD  3436  cbvrabv  3441  rabrab  3454  cbvrabw  3466  cbvrab  3472  cbvcsbw  3903  cbvcsb  3904  csbcow  3908  csbco  3909  cbvrabcsfw  3937  cbvrabcsf  3941  un4  4169  incom  4201  in13  4222  in31  4223  in4  4225  symdifcom  4243  indifcom  4272  indir  4275  undir  4276  indifdir  4284  difdif2  4286  notrab  4311  dfnul3  4326  dfnul3OLD  4328  dfif5  4544  rabsnifsb  4726  prcom  4736  tprot  4753  tpcoma  4754  tpcomb  4755  tpass  4756  qdassr  4758  pw0  4815  pwpw0  4816  pwsn  4900  pwsnOLD  4901  cbviun  5039  cbviin  5040  cbviung  5041  cbviing  5042  iunrab  5055  iunin1  5075  iinuni  5101  cbvopab  5220  cbvopabv  5221  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  cbvopab1v  5227  cbvopab2v  5229  unopab  5230  cbvmptf  5257  cbvmptfg  5258  cbvmptv  5261  iunopab  5559  iunopabOLD  5560  dfid4  5575  dfid2  5576  dfid3  5577  rabxp  5724  fconstmpt  5738  csbxp  5775  inxp  5832  cnvco  5885  csbdm  5897  rnmpt  5954  csbres  5984  resundi  5995  resundir  5996  resindi  5997  resindir  5998  rescom  6007  resima  6015  imadmrn  6069  cnvimarndm  6081  cnvi  6141  cnvin  6144  rnun  6145  imaundi  6149  cnvxp  6156  imainrect  6180  csbrn  6202  imacnvcnv  6205  resdmres  6231  imadmres  6233  resdifdir  6236  mptpreima  6237  dfpred3  6311  predin  6328  predun  6329  preddif  6330  frpoind  6343  wfiOLD  6352  cbviotaw  6502  cbviotavw  6503  cbviota  6505  sb8iota  6507  resdif  6854  opabiotadm  6973  fndmin  7046  fninfp  7174  cbvriotaw  7377  cbvriotavw  7378  cbvriota  7382  riotarab  7411  dfoprab2  7470  cbvoprab1  7499  cbvoprab2  7500  cbvoprab12  7501  cbvoprab3  7503  cbvmpox  7505  resoprab  7529  caov32  7638  caov31  7640  caov4  7642  caovlem2  7647  uniuni  7753  zfrep6  7945  ofmres  7975  dfopab2  8042  dfxp3  8051  dmmpossx  8056  fmpox  8057  fsplit  8108  ovtpos  8232  tposco  8248  frrlem5  8281  tfrlem10  8393  o2p2e4  8547  0map0sn0  8885  mapsncnv  8893  cbvixp  8914  xpcomco  9068  sbthlem6  9094  1sdomOLD  9255  ttrclresv  9718  frind  9751  cardf2  9944  alephcard  10071  alephfplem1  10105  xp2dju  10177  djuassen  10179  infdju1  10190  pwdju1  10191  ackbij1lem14  10234  compsscnv  10372  dffin1-5  10389  ituniiun  10423  axdc2lem  10449  axdc3lem4  10454  axcclem  10458  pwcfsdom  10584  dmaddpi  10891  dmmulpi  10892  adderpqlem  10955  addassnq  10959  mulcanenq  10961  addcmpblnr  11070  mulcmpblnrlem  11071  ltsrpr  11078  mulgt0sr  11106  sqgt0sr  11107  axi2m1  11160  negiso  12201  nummac  12729  decsubi  12747  9t11e99  12814  fztpval  13570  seqval  13984  sqrecii  14154  sqdivi  14156  binom2i  14183  4bc2eq6  14296  hashgval  14300  revs1  14722  cats1cat  14819  trclublem  14949  shftdm  15025  shftidt2  15035  cji  15113  cbvsum  15648  sumfc  15662  ackbijnn  15781  cbvprod  15866  prodfc  15896  fsumcube  16011  divalglem2  16345  nn0gcdsq  16695  prmreclem2  16857  prmrec  16862  hashbc0  16945  dec5nprm  17006  dec2nprm  17007  gcdi  17013  decexp2  17015  decsplit  17023  1259lem1  17071  1259lem4  17074  4001lem1  17081  phlstr  17298  oduval  18251  oduleval  18252  odubas  18254  odubasOLD  18255  lubdm  18314  glbdm  18327  oppgid  19271  symgbas0  19304  gsumcom2  19891  ringidval  20084  oppr1  20248  dfrhm2  20372  rmodislmod  20772  rmodislmodOLD  20773  cnfldsub  21262  cnflddiv  21264  dvdsrzring  21321  pjdm  21572  pjfval2  21574  opsrtoslem1  21927  restco  22988  ufprim  23733  tgioo3  24641  oprpiece1res1  24796  oprpiece1res2  24797  volfiniun  25396  vitalilem4  25460  cbvitg  25625  itgresr  25628  cbvditg  25703  plyid  26061  coeidp  26116  dgrid  26117  sincos3rdpi  26366  logblog  26638  ang180lem2  26656  1cubrlem  26687  asin1  26740  log2ublem2  26793  log2ublem3  26794  emcllem5  26845  lgsdir2lem5  27175  lgsquadlem3  27228  2lgslem1b  27238  2lgsoddprmlem3d  27259  noextend  27512  nosupbday  27551  nosupbnd1  27560  nosupbnd2  27562  noinfbday  27566  noinfbnd1  27575  dmscut  27657  madeval2  27693  negs0s  27852  cchhllem  28577  cchhllemOLD  28578  ax5seglem7  28626  vtxval0  28732  iedgval0  28733  finsumvtxdg2ssteplem1  29235  wwlksnfi  29593  1wlkdlem1  29823  ex-un  30110  ex-pw  30115  ex-cnv  30123  ex-co  30124  bafval  30290  vsfval  30319  cnnvba  30365  cnnvm  30368  ip2dii  30530  siilem1  30537  h2hcau  30665  hvsubsub4i  30745  hvnegdii  30748  normlem3  30798  normlem8  30803  norm-iii-i  30825  normpar2i  30842  polid2i  30843  chjassi  31172  chj4i  31209  h1de2i  31239  spanunsni  31265  fh3i  31309  fh4i  31310  qlax4i  31316  qlaxr3i  31322  3oalem5  31352  pjadjii  31360  pjsubii  31364  hoadd32i  31464  cnvadj  31578  hh0oi  31589  hhcno  31590  hhcnf  31591  nmopnegi  31651  lnophmlem2  31703  branmfn  31791  dmrab  32170  abrexexd  32179  cbviunf  32220  maprnin  32389  dpmul10  32494  dpexpp1  32507  dpadd3  32511  dpmul  32512  dpmul4  32513  psgnfzto1st  32700  cycpmconjs  32751  lmlimxrge0  33392  zrhre  33463  qqhre  33464  rrhre  33465  cbvesum  33504  unibrsiga  33648  eulerpartlemt  33834  eulerpartgbij  33835  ballotlemrinv  33996  hgt750lem2  34128  bnj1146  34266  bnj893  34403  bnj1234  34488  subfacp1lem1  34634  kur14lem2  34662  kur14lem5  34665  kur14lem7  34667  cvmscld  34728  satfv1lem  34817  fmla0  34837  mvtval  34955  mthmpps  35037  fixun  35351  bj-inrab  36271  bj-inrab3  36273  bj-gabeqis  36282  bj-pr1un  36348  bj-pr2un  36362  bj-dfid2ALT  36410  bj-mpomptALT  36464  rnmptsn  36680  f1omptsnlem  36681  rabiun  36925  phpreu  36936  poimirlem18  36970  ovoliunnfl  36994  voliunnfl  36996  mbfposadd  36999  asindmre  37035  abeqin  37584  rncnvepres  37636  qsresid  37658  rnxrn  37732  xrnres  37736  xrnres2  37737  xrnres3  37738  rncossdmcoss  37789  1cosscnvxrn  37809  refrelsredund4  37966  mpets  38176  cdleme25cv  39693  sn-iotalemcor  41506  sqdeccom12  41664  sumcubes  41674  nn0expgcd  41689  sn-00idlem2  41735  sn-1ticom  41770  mendsca  42394  areaquad  42428  onsucrn  42484  df3o2  42526  df3o3  42527  omcl3g  42547  dfno2  42642  cnvrcl0  42839  sqrtcvallem1  42845  trclrelexplem  42925  cbvmpo2  44248  cbvmpo1  44249  mptssid  44403  fprodabs2  44770  stoweidlem13  45188  wallispilem4  45243  fourierdlem94  45375  fourierdlem102  45383  fourierdlem111  45392  fourierdlem112  45393  fourierdlem113  45394  fourierdlem114  45395  41prothprmlem2  46745  2exp340mod341  46860  8exp8mod9  46863  nfermltl8rev  46869  cbvmpox2  47174  dmmpossx2  47175  zlmodzxzequa  47339  zlmodzxzequap  47342