Theorem 3eqtr4i 2778

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  rabbiiaOLD  3448  cbvrabv  3454  rabrab  3468  cbvrabw  3481  cbvrabwOLD  3482  cbvrab  3487  cbvcsbw  3931  cbvcsb  3932  cbvcsbv  3933  csbcow  3936  csbco  3937  cbvrabcsfw  3965  cbvrabcsf  3969  un4  4198  incom  4230  in13  4252  in31  4253  in4  4255  symdifcom  4273  indifcom  4302  indir  4305  undir  4306  indifdir  4314  difdif2  4315  notrab  4341  dfnul3  4356  dfnul3OLD  4358  dfif5  4564  rabsnifsb  4747  prcom  4757  tprot  4774  tpcoma  4775  tpcomb  4776  tpass  4777  qdassr  4779  pw0  4837  pwpw0  4838  pwsn  4924  cbviun  5059  cbviin  5060  cbviung  5061  cbviing  5062  cbviunv  5063  cbviinv  5064  iunrab  5075  iunin1  5095  iinuni  5121  cbvopab  5238  cbvopabv  5239  cbvopab1  5241  cbvopab1g  5242  cbvopab2  5243  cbvopab1s  5244  cbvopab1v  5245  cbvopab2v  5247  unopab  5248  cbvmptf  5275  cbvmptfg  5276  cbvmptv  5279  iunopab  5578  iunopabOLD  5579  dfid4  5594  dfid2  5595  dfid3  5596  rabxp  5748  fconstmpt  5762  csbxp  5799  inxpOLD  5857  cnvco  5910  csbdm  5922  rnmpt  5980  csbres  6012  resundi  6023  resundir  6024  resindi  6025  resindir  6026  rescom  6032  resima  6044  imadmrn  6099  cnvimarndm  6112  cnvi  6173  cnvin  6176  rnun  6177  imaundi  6181  cnvxp  6188  imainrect  6212  csbrn  6234  imacnvcnv  6237  resdmres  6263  imadmres  6265  resdifdir  6268  mptpreima  6269  dfpred3  6343  predin  6359  predun  6360  preddif  6361  frpoind  6374  wfiOLD  6383  cbviotaw  6532  cbviotavw  6533  cbviota  6535  sb8iota  6537  resdif  6883  opabiotadm  7003  fndmin  7078  fninfp  7208  cbvriotaw  7413  cbvriotavw  7414  cbvriota  7418  riotarab  7447  dfoprab2  7508  cbvoprab1  7537  cbvoprab2  7538  cbvoprab12  7539  cbvoprab12v  7540  cbvoprab3  7541  cbvoprab3v  7542  cbvmpox  7543  cbvmpov  7545  resoprab  7568  caov32  7677  caov31  7679  caov4  7681  caovlem2  7686  uniuni  7797  zfrep6  7995  ofmres  8025  dfopab2  8093  dfxp3  8102  dmmpossx  8107  fmpox  8108  fsplit  8158  ovtpos  8282  tposco  8298  frrlem5  8331  tfrlem10  8443  o2p2e4  8597  0map0sn0  8943  mapsncnv  8951  cbvixp  8972  cbvixpv  8973  xpcomco  9128  sbthlem6  9154  1sdomOLD  9312  ttrclresv  9786  frind  9819  cardf2  10012  alephcard  10139  alephfplem1  10173  xp2dju  10246  djuassen  10248  infdju1  10259  pwdju1  10260  ackbij1lem14  10301  compsscnv  10440  dffin1-5  10457  ituniiun  10491  axdc2lem  10517  axdc3lem4  10522  axcclem  10526  pwcfsdom  10652  dmaddpi  10959  dmmulpi  10960  adderpqlem  11023  addassnq  11027  mulcanenq  11029  addcmpblnr  11138  mulcmpblnrlem  11139  ltsrpr  11146  mulgt0sr  11174  sqgt0sr  11175  axi2m1  11228  negiso  12275  nummac  12803  decsubi  12821  9t11e99  12888  fztpval  13646  seqval  14063  sqrecii  14232  sqdivi  14234  binom2i  14261  4bc2eq6  14378  hashgval  14382  revs1  14813  cats1cat  14910  trclublem  15044  shftdm  15120  shftidt2  15130  cji  15208  cbvsum  15743  cbvsumv  15744  sumfc  15757  ackbijnn  15876  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  prodfc  15993  fsumcube  16108  divalglem2  16443  nn0expgcd  16611  nn0gcdsq  16799  prmreclem2  16964  prmrec  16969  hashbc0  17052  dec5nprm  17113  dec2nprm  17114  gcdi  17120  decexp2  17122  decsplit  17130  1259lem1  17178  1259lem4  17181  4001lem1  17188  phlstr  17405  oduval  18358  oduleval  18359  odubas  18361  odubasOLD  18362  lubdm  18421  glbdm  18434  oppgid  19399  symgbas0  19430  gsumcom2  20017  ringidval  20210  oppr1  20376  dfrhm2  20500  rmodislmod  20950  rmodislmodOLD  20951  cnfldsub  21433  cnflddiv  21436  cnflddivOLD  21437  dvdsrzring  21495  pjdm  21750  pjfval2  21752  opsrtoslem1  22102  restco  23193  ufprim  23938  tgioo3  24846  oprpiece1res1  25001  oprpiece1res2  25002  volfiniun  25601  vitalilem4  25665  cbvitg  25831  cbvitgv  25832  itgresr  25834  cbvditg  25909  plyid  26268  coeidp  26323  dgrid  26324  sincos3rdpi  26577  logblog  26853  ang180lem2  26871  1cubrlem  26902  asin1  26955  log2ublem2  27008  log2ublem3  27009  emcllem5  27061  lgsdir2lem5  27391  lgsquadlem3  27444  2lgslem1b  27454  2lgsoddprmlem3d  27475  noextend  27729  nosupbday  27768  nosupbnd1  27777  nosupbnd2  27779  noinfbday  27783  noinfbnd1  27792  dmscut  27874  madeval2  27910  negs0s  28076  negs1s  28077  1p1e2s  28418  cchhllem  28919  cchhllemOLD  28920  ax5seglem7  28968  vtxval0  29074  iedgval0  29075  finsumvtxdg2ssteplem1  29581  wwlksnfi  29939  1wlkdlem1  30169  ex-un  30456  ex-pw  30461  ex-cnv  30469  ex-co  30470  bafval  30636  vsfval  30665  cnnvba  30711  cnnvm  30714  ip2dii  30876  siilem1  30883  h2hcau  31011  hvsubsub4i  31091  hvnegdii  31094  normlem3  31144  normlem8  31149  norm-iii-i  31171  normpar2i  31188  polid2i  31189  chjassi  31518  chj4i  31555  h1de2i  31585  spanunsni  31611  fh3i  31655  fh4i  31656  qlax4i  31662  qlaxr3i  31668  3oalem5  31698  pjadjii  31706  pjsubii  31710  hoadd32i  31810  cnvadj  31924  hh0oi  31935  hhcno  31936  hhcnf  31937  nmopnegi  31997  lnophmlem2  32049  branmfn  32137  dmrab  32525  3unrab  32531  abrexexd  32537  cbviunf  32578  maprnin  32745  dpmul10  32859  dpexpp1  32872  dpadd3  32876  dpmul  32877  dpmul4  32878  psgnfzto1st  33098  cycpmconjs  33149  fracbas  33272  lmlimxrge0  33894  zrhre  33965  qqhre  33966  rrhre  33967  cbvesum  34006  cbvesumv  34007  unibrsiga  34150  eulerpartlemt  34336  eulerpartgbij  34337  ballotlemrinv  34498  hgt750lem2  34629  bnj1146  34767  bnj893  34904  bnj1234  34989  subfacp1lem1  35147  kur14lem2  35175  kur14lem5  35178  kur14lem7  35180  cvmscld  35241  satfv1lem  35330  fmla0  35350  mvtval  35468  mthmpps  35550  fixun  35873  rabeqbii  36158  iuneq12i  36159  iineq1i  36160  iineq12i  36161  riotaeqbii  36162  ixpeq1i  36164  sumeq2si  36166  prodeq2si  36168  itgeq12i  36170  ditgeq123i  36173  cbvcsbvw2  36197  cbviunvw2  36198  cbviinvw2  36199  cbvmptvw2  36200  cbvriotavw2  36202  cbvoprab1vw  36203  cbvoprab2vw  36204  cbvoprab123vw  36205  cbvoprab23vw  36206  cbvoprab13vw  36207  cbvmpovw2  36208  cbvmpo1vw2  36209  cbvmpo2vw2  36210  cbvixpvw2  36211  cbvprodvw2  36213  cbvitgvw2  36214  cbvditgvw2  36215  bj-inrab  36893  bj-inrab3  36895  bj-gabeqis  36904  bj-pr1un  36969  bj-pr2un  36983  bj-dfid2ALT  37031  bj-mpomptALT  37085  rnmptsn  37301  f1omptsnlem  37302  rabiun  37553  phpreu  37564  poimirlem18  37598  ovoliunnfl  37622  voliunnfl  37624  mbfposadd  37627  asindmre  37663  abeqin  38208  rncnvepres  38259  qsresid  38281  rnxrn  38354  xrnres  38358  xrnres2  38359  xrnres3  38360  rncossdmcoss  38411  1cosscnvxrn  38431  refrelsredund4  38588  mpets  38798  cdleme25cv  40315  sn-iotalemcor  42215  sqdeccom12  42278  sumcubes  42301  sn-00idlem2  42375  sn-1ticom  42410  mendsca  43146  areaquad  43177  onsucrn  43233  df3o2  43275  df3o3  43276  omcl3g  43296  dfno2  43390  cnvrcl0  43587  sqrtcvallem1  43593  trclrelexplem  43673  iuneq1i  44987  cbvmpo2  44999  cbvmpo1  45000  cbvrabv2w  45030  mptssid  45149  fprodabs2  45516  stoweidlem13  45934  wallispilem4  45989  fourierdlem94  46121  fourierdlem102  46129  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fourierdlem114  46141  41prothprmlem2  47492  2exp340mod341  47607  8exp8mod9  47610  nfermltl8rev  47616  cbvmpox2  48060  dmmpossx2  48061  zlmodzxzequa  48225  zlmodzxzequap  48228