Theorem 3eqtr4i 2771

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 2764	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2764	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  rabbiiaOLD  3438  cbvrabv  3443  rabrab  3456  cbvrabw  3468  cbvrab  3474  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  5723  fconstmpt  5737  csbxp  5774  inxp  5831  cnvco  5884  csbdm  5896  rnmpt  5953  csbres  5983  resundi  5994  resundir  5995  resindi  5996  resindir  5997  rescom  6006  resima  6014  imadmrn  6068  cnvimarndm  6079  cnvi  6139  cnvin  6142  rnun  6143  imaundi  6147  cnvxp  6154  imainrect  6178  csbrn  6200  imacnvcnv  6203  resdmres  6229  imadmres  6231  resdifdir  6234  mptpreima  6235  dfpred3  6309  predin  6326  predun  6327  preddif  6328  frpoind  6341  wfiOLD  6350  cbviotaw  6500  cbviotavw  6501  cbviota  6503  sb8iota  6505  resdif  6852  opabiotadm  6971  fndmin  7044  fninfp  7169  cbvriotaw  7371  cbvriotavw  7372  cbvriota  7376  riotarab  7405  dfoprab2  7464  cbvoprab1  7493  cbvoprab2  7494  cbvoprab12  7495  cbvoprab3  7497  cbvmpox  7499  resoprab  7523  caov32  7631  caov31  7633  caov4  7635  caovlem2  7640  uniuni  7746  zfrep6  7938  ofmres  7968  dfopab2  8035  dfxp3  8044  dmmpossx  8049  fmpox  8050  fsplit  8100  ovtpos  8223  tposco  8239  frrlem5  8272  tfrlem10  8384  o2p2e4  8538  0map0sn0  8876  mapsncnv  8884  cbvixp  8905  xpcomco  9059  sbthlem6  9085  1sdomOLD  9246  ttrclresv  9709  frind  9742  cardf2  9935  alephcard  10062  alephfplem1  10096  xp2dju  10168  djuassen  10170  infdju1  10181  pwdju1  10182  ackbij1lem14  10225  compsscnv  10363  dffin1-5  10380  ituniiun  10414  axdc2lem  10440  axdc3lem4  10445  axcclem  10449  pwcfsdom  10575  dmaddpi  10882  dmmulpi  10883  adderpqlem  10946  addassnq  10950  mulcanenq  10952  addcmpblnr  11061  mulcmpblnrlem  11062  ltsrpr  11069  mulgt0sr  11097  sqgt0sr  11098  axi2m1  11151  negiso  12191  nummac  12719  decsubi  12737  9t11e99  12804  fztpval  13560  seqval  13974  sqrecii  14144  sqdivi  14146  binom2i  14173  4bc2eq6  14286  hashgval  14290  revs1  14712  cats1cat  14809  trclublem  14939  shftdm  15015  shftidt2  15025  cji  15103  cbvsum  15638  sumfc  15652  ackbijnn  15771  cbvprod  15856  prodfc  15886  fsumcube  16001  divalglem2  16335  nn0gcdsq  16685  prmreclem2  16847  prmrec  16852  hashbc0  16935  dec5nprm  16996  dec2nprm  16997  gcdi  17003  decexp2  17005  decsplit  17013  1259lem1  17061  1259lem4  17064  4001lem1  17071  phlstr  17288  oduval  18238  oduleval  18239  odubas  18241  odubasOLD  18242  lubdm  18301  glbdm  18314  oppgid  19218  symgbas0  19251  gsumcom2  19838  ringidval  20001  oppr1  20157  dfrhm2  20246  rmodislmod  20533  rmodislmodOLD  20534  cnfldsub  20966  cnflddiv  20968  dvdsrzring  21023  pjdm  21254  pjfval2  21256  opsrtoslem1  21608  restco  22660  ufprim  23405  tgioo3  24313  oprpiece1res1  24459  oprpiece1res2  24460  volfiniun  25056  vitalilem4  25120  cbvitg  25285  itgresr  25288  cbvditg  25363  plyid  25715  coeidp  25769  dgrid  25770  sincos3rdpi  26018  logblog  26287  ang180lem2  26305  1cubrlem  26336  asin1  26389  log2ublem2  26442  log2ublem3  26443  emcllem5  26494  lgsdir2lem5  26822  lgsquadlem3  26875  2lgslem1b  26885  2lgsoddprmlem3d  26906  noextend  27159  nosupbday  27198  nosupbnd1  27207  nosupbnd2  27209  noinfbday  27213  noinfbnd1  27222  dmscut  27302  madeval2  27338  negs0s  27491  cchhllem  28134  cchhllemOLD  28135  ax5seglem7  28183  vtxval0  28289  iedgval0  28290  finsumvtxdg2ssteplem1  28792  wwlksnfi  29150  1wlkdlem1  29380  ex-un  29667  ex-pw  29672  ex-cnv  29680  ex-co  29681  bafval  29845  vsfval  29874  cnnvba  29920  cnnvm  29923  ip2dii  30085  siilem1  30092  h2hcau  30220  hvsubsub4i  30300  hvnegdii  30303  normlem3  30353  normlem8  30358  norm-iii-i  30380  normpar2i  30397  polid2i  30398  chjassi  30727  chj4i  30764  h1de2i  30794  spanunsni  30820  fh3i  30864  fh4i  30865  qlax4i  30871  qlaxr3i  30877  3oalem5  30907  pjadjii  30915  pjsubii  30919  hoadd32i  31019  cnvadj  31133  hh0oi  31144  hhcno  31145  hhcnf  31146  nmopnegi  31206  lnophmlem2  31258  branmfn  31346  dmrab  31725  abrexexd  31734  cbviunf  31775  maprnin  31944  dpmul10  32049  dpexpp1  32062  dpadd3  32066  dpmul  32067  dpmul4  32068  psgnfzto1st  32252  cycpmconjs  32303  lmlimxrge0  32917  zrhre  32988  qqhre  32989  rrhre  32990  cbvesum  33029  unibrsiga  33173  eulerpartlemt  33359  eulerpartgbij  33360  ballotlemrinv  33521  hgt750lem2  33653  bnj1146  33791  bnj893  33928  bnj1234  34013  subfacp1lem1  34159  kur14lem2  34187  kur14lem5  34190  kur14lem7  34192  cvmscld  34253  satfv1lem  34342  fmla0  34362  mvtval  34480  mthmpps  34562  fixun  34870  bj-inrab  35796  bj-inrab3  35798  bj-gabeqis  35807  bj-pr1un  35873  bj-pr2un  35887  bj-dfid2ALT  35935  bj-mpomptALT  35989  rnmptsn  36205  f1omptsnlem  36206  rabiun  36450  phpreu  36461  poimirlem18  36495  ovoliunnfl  36519  voliunnfl  36521  mbfposadd  36524  asindmre  36560  abeqin  37109  rncnvepres  37161  qsresid  37183  rnxrn  37257  xrnres  37261  xrnres2  37262  xrnres3  37263  rncossdmcoss  37314  1cosscnvxrn  37334  refrelsredund4  37491  mpets  37701  cdleme25cv  39218  sn-iotalemcor  41036  sqdeccom12  41199  sumcubes  41207  nn0expgcd  41222  sn-00idlem2  41269  sn-1ticom  41304  mendsca  41917  areaquad  41951  onsucrn  42007  df3o2  42049  df3o3  42050  omcl3g  42070  dfno2  42165  cnvrcl0  42362  sqrtcvallem1  42368  trclrelexplem  42448  cbvmpo2  43772  cbvmpo1  43773  mptssid  43930  fprodabs2  44298  stoweidlem13  44716  wallispilem4  44771  fourierdlem94  44903  fourierdlem102  44911  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  fourierdlem114  44923  41prothprmlem2  46273  2exp340mod341  46388  8exp8mod9  46391  nfermltl8rev  46397  cbvmpox2  46965  dmmpossx2  46966  zlmodzxzequa  47131  zlmodzxzequap  47134