Theorem 3eqtr4i 2796

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

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  cbvrabv  3426  cbvrabw  3451  cbvrab  3454  cbvcsbw  3863  cbvcsb  3864  cbvcsbv  3865  csbcow  3868  csbco  3869  cbvrabcsfw  3894  cbvrabcsf  3898  un4  4128  incom  4162  in13  4183  in31  4184  in4  4186  symdifcom  4207  indifcom  4236  indir  4239  undir  4240  indifdir  4248  difdif2  4249  notrab  4275  dfnul3  4290  dfif5  4504  rabsnifsb  4688  prcom  4698  tprot  4715  tpcoma  4716  tpcomb  4717  tpass  4718  qdassr  4720  pw0  4778  pwpw0  4779  pwsn  4865  cbviun  4999  cbviin  5000  cbviung  5001  cbviing  5002  cbviunv  5003  cbviinv  5004  iunrab  5017  iunin1  5036  iinuni  5064  cbvopab  5183  cbvopabv  5184  cbvopab1  5185  cbvopab1g  5186  cbvopab2  5187  cbvopab1s  5188  cbvopab1v  5189  cbvopab2v  5190  unopab  5191  cbvmptf  5211  cbvmptfg  5212  cbvmptv  5215  iunopab  5544  dfid4  5557  dfid2  5558  dfid3  5559  rabxp  5709  fconstmpt  5723  csbxp  5762  cnvi  5871  cnvco  5875  csbdm  5887  rnmpt  5947  csbres  5981  resundi  5992  resundir  5993  resindi  5994  resindir  5995  rescom  6001  resima  6014  imadmrn  6072  cnvimarndm  6085  cnvin  6141  rnun  6142  imaundi  6147  cnvxp  6154  imainrect  6179  csbrn  6204  imacnvcnv  6207  resdmres  6233  imadmres  6235  resdifdir  6238  mptpreima  6239  dfpred3  6313  predin  6328  predun  6329  preddif  6330  frpoind  6343  cbviotaw  6499  cbviotavw  6500  cbviota  6501  sb8iota  6503  resdif  6842  opabiotadm  6962  fndmin  7040  fninfp  7172  cbvriotaw  7376  cbvriotavw  7377  cbvriota  7380  riotarab  7409  dfoprab2  7468  cbvoprab1  7497  cbvoprab2  7498  cbvoprab12  7499  cbvoprab12v  7500  cbvoprab3  7501  cbvoprab3v  7502  cbvmpox  7503  cbvmpov  7505  resoprab  7528  caov32  7637  caov31  7639  caov4  7641  caovlem2  7646  uniuni  7757  zfrep6OLD  7948  ofmres  7977  dfopab2  8045  dfxp3  8054  dmmpossx  8059  fmpox  8060  fsplit  8108  ovtpos  8233  tposco  8249  frrlem5  8283  tfrlem10  8370  o2p2e4  8522  0map0sn0  8879  mapsncnv  8887  cbvixp  8908  cbvixpv  8909  xpcomco  9051  sbthlem6  9076  ttrclresv  9682  frind  9718  cardf2  9925  alephcard  10050  alephfplem1  10084  xp2dju  10156  djuassen  10158  infdju1  10169  pwdju1  10170  ackbij1lem14  10211  compsscnv  10350  dffin1-5  10367  ituniiun  10401  axdc2lem  10427  axdc3lem4  10432  axcclem  10436  pwcfsdom  10563  dmaddpi  10870  dmmulpi  10871  adderpqlem  10934  addassnq  10938  mulcanenq  10940  addcmpblnr  11049  mulcmpblnrlem  11050  ltsrpr  11057  mulgt0sr  11085  sqgt0sr  11086  axi2m1  11139  negiso  12190  nummac  12756  decsubi  12774  9t11e99OLD  12842  fztpval  13610  seqval  14044  sqrecii  14215  sqdivi  14217  binom2i  14244  4bc2eq6  14361  hashgval  14365  revs1  14798  cats1cat  14894  trclublem  15028  shftdm  15104  shftidt2  15114  cji  15206  cbvsum  15742  cbvsumv  15743  sumfc  15756  ackbijnn  15878  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  prodfc  15995  fsumcube  16109  divalglem2  16448  nn0expgcd  16617  nn0gcdsq  16806  prmreclem2  16972  prmrec  16977  hashbc0  17060  dec5nprm  17121  dec2nprm  17122  gcdi  17128  decsplit  17137  1259lem1  17186  1259lem4  17189  4001lem1  17196  phlstr  17394  oduval  18339  oduleval  18340  odubas  18342  lubdm  18400  glbdm  18413  oppgid  19421  symgbas0  19454  gsumcom2  20040  ringidval  20260  oppr1  20428  dfrhm2  20552  rmodislmod  21051  cnfldsub  21550  cnflddiv  21552  dvdsrzring  21611  pjdm  21857  pjfval2  21859  opsrtoslem1  22206  restco  23321  ufprim  24066  tgioo3  24963  oprpiece1res1  25110  oprpiece1res2  25111  volfiniun  25706  vitalilem4  25770  cbvitg  25935  cbvitgv  25936  itgresr  25938  cbvditg  26013  plyid  26366  coeidp  26420  dgrid  26421  sincos3rdpi  26682  logblog  26957  ang180lem2  26975  1cubrlem  27006  asin1  27059  log2ublem2  27112  log2ublem3  27113  emcllem5  27164  lgsdir2lem5  27493  lgsquadlem3  27546  2lgslem1b  27556  2lgsoddprmlem3d  27577  noextend  27830  nosupbday  27869  nosupbnd1  27878  nosupbnd2  27880  noinfbday  27884  noinfbnd1  27893  dmcuts  27984  madeval2  28026  neg0s  28219  neg1s  28220  cchhllem  29236  ax5seglem7  29285  vtxval0  29389  iedgval0  29390  finsumvtxdg2ssteplem1  29895  wwlksnfi  30255  1wlkdlem1  30488  ex-un  30775  ex-pw  30780  ex-cnv  30788  ex-co  30789  bafval  30956  vsfval  30985  cnnvba  31031  cnnvm  31034  ip2dii  31196  siilem1  31203  h2hcau  31331  hvsubsub4i  31411  hvnegdii  31414  normlem3  31464  normlem8  31469  norm-iii-i  31491  normpar2i  31508  polid2i  31509  chjassi  31838  chj4i  31875  h1de2i  31905  spanunsni  31931  fh3i  31975  fh4i  31976  qlax4i  31982  qlaxr3i  31988  3oalem5  32018  pjadjii  32026  pjsubii  32030  hoadd32i  32130  cnvadj  32244  hh0oi  32255  hhcno  32256  hhcnf  32257  nmopnegi  32317  lnophmlem2  32369  branmfn  32457  dmrab  32843  3unrab  32849  abrexexd  32855  cbviunf  32900  maprnin  33076  dpmul10  33214  dpexpp1  33227  dpadd3  33231  dpmul  33232  dpmul4  33233  psgnfzto1st  33425  cycpmconjs  33476  fracbas  33626  cos9thpiminplylem5  34176  lmlimxrge0  34338  zrhre  34409  qqhre  34410  rrhre  34411  cbvesum  34432  cbvesumv  34433  unibrsiga  34576  eulerpartlemt  34761  eulerpartgbij  34762  ballotlemrinv  34924  hgt750lem2  35039  bnj1146  35179  bnj893  35316  bnj1234  35401  r11  35487  r12  35488  subfacp1lem1  35671  kur14lem2  35699  kur14lem5  35702  kur14lem7  35704  cvmscld  35765  satfv1lem  35854  fmla0  35874  mvtval  35992  mthmpps  36074  fixun  36399  rabeqbii  36726  iuneq12i  36727  iineq1i  36728  iineq12i  36729  riotaeqbii  36730  ixpeq1i  36732  sumeq2si  36734  prodeq2si  36736  itgeq12i  36738  ditgeq123i  36741  cbvcsbvw2  36763  cbviunvw2  36764  cbviinvw2  36765  cbvmptvw2  36766  cbvriotavw2  36768  cbvoprab1vw  36769  cbvoprab2vw  36770  cbvoprab123vw  36771  cbvoprab23vw  36772  cbvoprab13vw  36773  cbvmpovw2  36774  cbvmpo1vw2  36775  cbvmpo2vw2  36776  cbvixpvw2  36777  cbvprodvw2  36779  cbvitgvw2  36780  cbvditgvw2  36781  ttcun  37043  ttciun  37045  bj-inrab  37583  bj-inrab3  37585  bj-gabeqis  37594  bj-pr1un  37659  bj-pr2un  37673  bj-dfid2ALT  37721  bj-mpomptALT  37781  rnmptsn  38001  f1omptsnlem  38002  rabiun  38264  phpreu  38275  poimirlem18  38309  ovoliunnfl  38333  voliunnfl  38335  mbfposadd  38338  asindmre  38374  abeqin  38923  rncnvepres  38978  qsresid  39000  dmxrn  39056  rnxrn  39090  xrnres  39094  xrnres2  39095  xrnres3  39096  dmxrncnvepres2  39102  dfsucmap3  39132  dfsucmap2  39133  rncossdmcoss  39214  1cosscnvxrn  39234  refrelsredund4  39385  mpets  39625  dfpetparts2  39641  dfpeters2  39643  petseq  39645  pets2eq  39646  cdleme25cv  41152  sn-iotalemcor  43013  sqdeccom12  43070  sumcubes  43094  resuppsinopn  43144  sn-00idlem2  43180  sn-1ticom  43216  mendsca  43932  areaquad  43963  onsucrn  44018  df3o2  44060  df3o3  44061  omcl3g  44081  dfno2  44174  cnvrcl0  44371  sqrtcvallem1  44377  trclrelexplem  44457  iuneq1i  45824  cbvmpo2  45835  cbvmpo1  45836  cbvrabv2w  45866  mptssid  45976  fprodabs2  46331  stoweidlem13  46747  wallispilem4  46802  fourierdlem94  46934  fourierdlem102  46942  fourierdlem111  46951  fourierdlem112  46952  fourierdlem113  46953  fourierdlem114  46954  41prothprmlem2  48390  2exp340mod341  48518  8exp8mod9  48521  nfermltl8rev  48527  stgr1  48746  gpgprismgr4cycllem6  48885  gpgprismgr4cycllem9  48888  gpgprismgr4cycllem10  48889  cbvmpox2  49136  dmmpossx2  49137  zlmodzxzequa  49296  zlmodzxzequap  49299  resinsn  49670  dfswapf2  50059