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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  cbvrabv  3399  cbvrabw  3424  cbvrabwOLD  3425  cbvrab  3428  cbvcsbw  3847  cbvcsb  3848  cbvcsbv  3849  csbcow  3852  csbco  3853  cbvrabcsfw  3878  cbvrabcsf  3882  un4  4115  incom  4149  in13  4171  in31  4172  in4  4174  symdifcom  4194  indifcom  4223  indir  4226  undir  4227  indifdir  4235  difdif2  4236  notrab  4262  dfnul3  4277  dfif5  4483  rabsnifsb  4666  prcom  4676  tprot  4693  tpcoma  4694  tpcomb  4695  tpass  4696  qdassr  4698  pw0  4755  pwpw0  4756  pwsn  4843  cbviun  4977  cbviin  4978  cbviung  4979  cbviing  4980  cbviunv  4981  cbviinv  4982  iunrab  4995  iunin1  5014  iinuni  5040  cbvopab  5157  cbvopabv  5158  cbvopab1  5159  cbvopab1g  5160  cbvopab2  5161  cbvopab1s  5162  cbvopab1v  5163  cbvopab2v  5164  unopab  5165  cbvmptf  5185  cbvmptfg  5186  cbvmptv  5189  iunopab  5514  dfid4  5527  dfid2  5528  dfid3  5529  rabxp  5679  fconstmpt  5693  csbxp  5732  cnvco  5840  csbdm  5852  rnmpt  5912  csbres  5947  resundi  5958  resundir  5959  resindi  5960  resindir  5961  rescom  5967  resima  5980  imadmrn  6035  cnvimarndm  6048  cnvi  6105  cnvin  6108  rnun  6109  imaundi  6113  cnvxp  6121  imainrect  6145  csbrn  6167  imacnvcnv  6170  resdmres  6196  imadmres  6198  resdifdir  6201  mptpreima  6202  dfpred3  6276  predin  6291  predun  6292  preddif  6293  frpoind  6306  cbviotaw  6461  cbviotavw  6462  cbviota  6463  sb8iota  6465  resdif  6801  opabiotadm  6921  fndmin  6997  fninfp  7129  cbvriotaw  7333  cbvriotavw  7334  cbvriota  7337  riotarab  7366  dfoprab2  7425  cbvoprab1  7454  cbvoprab2  7455  cbvoprab12  7456  cbvoprab12v  7457  cbvoprab3  7458  cbvoprab3v  7459  cbvmpox  7460  cbvmpov  7462  resoprab  7485  caov32  7594  caov31  7596  caov4  7598  caovlem2  7603  uniuni  7716  zfrep6OLD  7908  ofmres  7937  dfopab2  8005  dfxp3  8014  dmmpossx  8019  fmpox  8020  fsplit  8067  ovtpos  8191  tposco  8207  frrlem5  8240  tfrlem10  8326  o2p2e4  8476  0map0sn0  8833  mapsncnv  8841  cbvixp  8862  cbvixpv  8863  xpcomco  9005  sbthlem6  9030  ttrclresv  9638  frind  9674  cardf2  9867  alephcard  9992  alephfplem1  10026  xp2dju  10099  djuassen  10101  infdju1  10112  pwdju1  10113  ackbij1lem14  10154  compsscnv  10293  dffin1-5  10310  ituniiun  10344  axdc2lem  10370  axdc3lem4  10375  axcclem  10379  pwcfsdom  10506  dmaddpi  10813  dmmulpi  10814  adderpqlem  10877  addassnq  10881  mulcanenq  10883  addcmpblnr  10992  mulcmpblnrlem  10993  ltsrpr  11000  mulgt0sr  11028  sqgt0sr  11029  axi2m1  11082  negiso  12136  nummac  12689  decsubi  12707  9t11e99  12774  fztpval  13540  seqval  13974  sqrecii  14145  sqdivi  14147  binom2i  14174  4bc2eq6  14291  hashgval  14295  revs1  14727  cats1cat  14823  trclublem  14957  shftdm  15033  shftidt2  15043  cji  15121  cbvsum  15657  cbvsumv  15658  sumfc  15671  ackbijnn  15793  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  prodfc  15910  fsumcube  16025  divalglem2  16364  nn0expgcd  16533  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  18254  oduleval  18255  odubas  18257  lubdm  18315  glbdm  18328  oppgid  19331  symgbas0  19364  gsumcom2  19950  ringidval  20164  oppr1  20330  dfrhm2  20454  rmodislmod  20925  cnfldsub  21380  cnflddiv  21382  dvdsrzring  21441  pjdm  21687  pjfval2  21689  opsrtoslem1  22033  restco  23129  ufprim  23874  tgioo3  24771  oprpiece1res1  24918  oprpiece1res2  24919  volfiniun  25514  vitalilem4  25578  cbvitg  25743  cbvitgv  25744  itgresr  25746  cbvditg  25821  plyid  26174  coeidp  26228  dgrid  26229  sincos3rdpi  26481  logblog  26756  ang180lem2  26774  1cubrlem  26805  asin1  26858  log2ublem2  26911  log2ublem3  26912  emcllem5  26963  lgsdir2lem5  27292  lgsquadlem3  27345  2lgslem1b  27355  2lgsoddprmlem3d  27376  noextend  27630  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfbday  27684  noinfbnd1  27693  dmcuts  27783  madeval2  27825  neg0s  28018  neg1s  28019  cchhllem  28955  ax5seglem7  29004  vtxval0  29108  iedgval0  29109  finsumvtxdg2ssteplem1  29614  wwlksnfi  29974  1wlkdlem1  30207  ex-un  30494  ex-pw  30499  ex-cnv  30507  ex-co  30508  bafval  30675  vsfval  30704  cnnvba  30750  cnnvm  30753  ip2dii  30915  siilem1  30922  h2hcau  31050  hvsubsub4i  31130  hvnegdii  31133  normlem3  31183  normlem8  31188  norm-iii-i  31210  normpar2i  31227  polid2i  31228  chjassi  31557  chj4i  31594  h1de2i  31624  spanunsni  31650  fh3i  31694  fh4i  31695  qlax4i  31701  qlaxr3i  31707  3oalem5  31737  pjadjii  31745  pjsubii  31749  hoadd32i  31849  cnvadj  31963  hh0oi  31974  hhcno  31975  hhcnf  31976  nmopnegi  32036  lnophmlem2  32088  branmfn  32176  dmrab  32566  3unrab  32573  abrexexd  32579  cbviunf  32625  maprnin  32804  dpmul10  32954  dpexpp1  32967  dpadd3  32971  dpmul  32972  dpmul4  32973  psgnfzto1st  33166  cycpmconjs  33217  fracbas  33366  cos9thpiminplylem5  33930  lmlimxrge0  34092  zrhre  34163  qqhre  34164  rrhre  34165  cbvesum  34186  cbvesumv  34187  unibrsiga  34330  eulerpartlemt  34515  eulerpartgbij  34516  ballotlemrinv  34678  hgt750lem2  34796  bnj1146  34933  bnj893  35070  bnj1234  35155  r11  35237  r12  35238  subfacp1lem1  35361  kur14lem2  35389  kur14lem5  35392  kur14lem7  35394  cvmscld  35455  satfv1lem  35544  fmla0  35564  mvtval  35682  mthmpps  35764  fixun  36089  rabeqbii  36376  iuneq12i  36377  iineq1i  36378  iineq12i  36379  riotaeqbii  36380  ixpeq1i  36382  sumeq2si  36384  prodeq2si  36386  itgeq12i  36388  ditgeq123i  36391  cbvcsbvw2  36413  cbviunvw2  36414  cbviinvw2  36415  cbvmptvw2  36416  cbvriotavw2  36418  cbvoprab1vw  36419  cbvoprab2vw  36420  cbvoprab123vw  36421  cbvoprab23vw  36422  cbvoprab13vw  36423  cbvmpovw2  36424  cbvmpo1vw2  36425  cbvmpo2vw2  36426  cbvixpvw2  36427  cbvprodvw2  36429  cbvitgvw2  36430  cbvditgvw2  36431  ttcun  36694  ttciun  36696  bj-inrab  37234  bj-inrab3  37236  bj-gabeqis  37245  bj-pr1un  37310  bj-pr2un  37324  bj-dfid2ALT  37372  bj-mpomptALT  37431  rnmptsn  37651  f1omptsnlem  37652  rabiun  37914  phpreu  37925  poimirlem18  37959  ovoliunnfl  37983  voliunnfl  37985  mbfposadd  37988  asindmre  38024  abeqin  38575  rncnvepres  38630  qsresid  38652  dmxrn  38708  rnxrn  38742  xrnres  38746  xrnres2  38747  xrnres3  38748  dmxrncnvepres2  38754  dfsucmap3  38784  dfsucmap2  38785  rncossdmcoss  38866  1cosscnvxrn  38886  refrelsredund4  39037  mpets  39277  dfpetparts2  39293  dfpeters2  39295  petseq  39297  pets2eq  39298  cdleme25cv  40804  sn-iotalemcor  42663  sqdeccom12  42721  sumcubes  42745  resuppsinopn  42795  sn-00idlem2  42831  sn-1ticom  42867  mendsca  43613  areaquad  43644  onsucrn  43699  df3o2  43741  df3o3  43742  omcl3g  43762  dfno2  43855  cnvrcl0  44052  sqrtcvallem1  44058  trclrelexplem  44138  iuneq1i  45515  cbvmpo2  45527  cbvmpo1  45528  cbvrabv2w  45558  mptssid  45670  fprodabs2  46025  stoweidlem13  46441  wallispilem4  46496  fourierdlem94  46628  fourierdlem102  46636  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fourierdlem114  46648  41prothprmlem2  48081  2exp340mod341  48209  8exp8mod9  48212  nfermltl8rev  48218  stgr1  48437  gpgprismgr4cycllem6  48576  gpgprismgr4cycllem9  48579  gpgprismgr4cycllem10  48580  cbvmpox2  48812  dmmpossx2  48813  zlmodzxzequa  48972  zlmodzxzequap  48975  resinsn  49347  dfswapf2  49736