Theorem 3eqtr4i 2776

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  rabrab  3305  rabbiia  3396  cbvrabw  3414  cbvrab  3415  cbvrabv  3416  cbvcsbw  3838  cbvcsb  3839  csbcow  3843  csbco  3844  cbvrabcsfw  3872  cbvrabcsf  3876  un4  4099  incom  4131  in13  4153  in31  4154  in4  4156  symdifcom  4174  indifcom  4203  indir  4206  undir  4207  indifdir  4215  difdif2  4217  notrab  4242  dfnul3  4257  dfnul3OLD  4259  dfif5  4472  rabsnifsb  4655  prcom  4665  tprot  4682  tpcoma  4683  tpcomb  4684  tpass  4685  qdassr  4687  pw0  4742  pwpw0  4743  pwsn  4828  pwsnOLD  4829  cbviun  4962  cbviin  4963  cbviung  4964  cbviing  4965  iunrab  4978  iunin1  4997  iinuni  5023  cbvopab  5142  cbvopabv  5143  cbvopab1  5145  cbvopab1g  5146  cbvopab2  5147  cbvopab1s  5148  cbvopab1v  5149  cbvopab2v  5151  unopab  5152  cbvmptf  5179  cbvmptfg  5180  cbvmptv  5183  iunopab  5465  dfid4  5481  dfid2  5482  dfid3  5483  rabxp  5626  fconstmpt  5640  csbxp  5676  inxp  5730  cnvco  5783  csbdm  5795  rnmpt  5853  csbres  5883  resundi  5894  resundir  5895  resindi  5896  resindir  5897  rescom  5906  resima  5914  imadmrn  5968  cnvimarndm  5979  cnvi  6034  cnvin  6037  rnun  6038  imaundi  6042  cnvxp  6049  imainrect  6073  csbrn  6095  imacnvcnv  6098  resdmres  6124  imadmres  6126  resdifdir  6129  mptpreima  6130  dfpred3  6202  predin  6219  predun  6220  preddif  6221  frpoind  6230  wfiOLD  6239  cbviotaw  6383  cbviotavw  6384  cbviota  6386  sb8iota  6388  resdif  6720  opabiotadm  6832  fndmin  6904  fninfp  7028  cbvriotaw  7221  cbvriotavw  7222  cbvriota  7226  dfoprab2  7311  cbvoprab1  7340  cbvoprab2  7341  cbvoprab12  7342  cbvoprab3  7344  cbvmpox  7346  resoprab  7370  caov32  7477  caov31  7479  caov4  7481  caovlem2  7486  uniuni  7590  zfrep6  7771  ofmres  7800  dfopab2  7865  dfxp3  7874  dmmpossx  7879  fmpox  7880  fsplit  7928  fsplitOLD  7929  ovtpos  8028  tposco  8044  frrlem5  8077  tfrlem10  8189  o2p2e4  8333  o2p2e4OLD  8334  0map0sn0  8631  mapsncnv  8639  cbvixp  8660  xpcomco  8802  sbthlem6  8828  1sdom  8955  frind  9439  cardf2  9632  alephcard  9757  alephfplem1  9791  xp2dju  9863  djuassen  9865  infdju1  9876  pwdju1  9877  ackbij1lem14  9920  compsscnv  10058  dffin1-5  10075  ituniiun  10109  axdc2lem  10135  axdc3lem4  10140  axcclem  10144  pwcfsdom  10270  dmaddpi  10577  dmmulpi  10578  adderpqlem  10641  addassnq  10645  mulcanenq  10647  addcmpblnr  10756  mulcmpblnrlem  10757  ltsrpr  10764  mulgt0sr  10792  sqgt0sr  10793  axi2m1  10846  negiso  11885  nummac  12411  decsubi  12429  9t11e99  12496  fztpval  13247  seqval  13660  sqrecii  13828  sqdivi  13830  binom2i  13856  4bc2eq6  13971  hashgval  13975  revs1  14406  cats1cat  14502  trclublem  14634  shftdm  14710  shftidt2  14720  cji  14798  cbvsum  15335  sumfc  15349  ackbijnn  15468  cbvprod  15553  prodfc  15583  fsumcube  15698  divalglem2  16032  nn0gcdsq  16384  prmreclem2  16546  prmrec  16551  hashbc0  16634  dec5nprm  16695  dec2nprm  16696  gcdi  16702  decexp2  16704  decsplit  16712  1259lem1  16760  1259lem4  16763  4001lem1  16770  phlstr  16981  oduval  17922  oduleval  17923  odubas  17925  lubdm  17984  glbdm  17997  oppgid  18878  symgbas0  18911  gsumcom2  19491  ringidval  19654  oppr1  19791  dfrhm2  19876  rmodislmod  20106  rmodislmodOLD  20107  cnfldsub  20538  cnflddiv  20540  dvdsrzring  20595  pjdm  20824  pjfval2  20826  opsrtoslem1  21172  restco  22223  ufprim  22968  tgioo3  23874  oprpiece1res1  24020  oprpiece1res2  24021  volfiniun  24616  vitalilem4  24680  cbvitg  24845  itgresr  24848  cbvditg  24923  plyid  25275  coeidp  25329  dgrid  25330  sincos3rdpi  25578  logblog  25847  ang180lem2  25865  1cubrlem  25896  asin1  25949  log2ublem2  26002  log2ublem3  26003  emcllem5  26054  lgsdir2lem5  26382  lgsquadlem3  26435  2lgslem1b  26445  2lgsoddprmlem3d  26466  cchhllem  27157  cchhllemOLD  27158  ax5seglem7  27206  vtxval0  27312  iedgval0  27313  finsumvtxdg2ssteplem1  27815  wwlksnfi  28172  1wlkdlem1  28402  ex-un  28689  ex-pw  28694  ex-cnv  28702  ex-co  28703  bafval  28867  vsfval  28896  cnnvba  28942  cnnvm  28945  ip2dii  29107  siilem1  29114  h2hcau  29242  hvsubsub4i  29322  hvnegdii  29325  normlem3  29375  normlem8  29380  norm-iii-i  29402  normpar2i  29419  polid2i  29420  chjassi  29749  chj4i  29786  h1de2i  29816  spanunsni  29842  fh3i  29886  fh4i  29887  qlax4i  29893  qlaxr3i  29899  3oalem5  29929  pjadjii  29937  pjsubii  29941  hoadd32i  30041  cnvadj  30155  hh0oi  30166  hhcno  30167  hhcnf  30168  nmopnegi  30228  lnophmlem2  30280  branmfn  30368  dmrab  30745  abrexexd  30755  cbviunf  30796  maprnin  30968  dpmul10  31071  dpexpp1  31084  dpadd3  31088  dpmul  31089  dpmul4  31090  psgnfzto1st  31274  cycpmconjs  31325  lmlimxrge0  31800  zrhre  31869  qqhre  31870  rrhre  31871  cbvesum  31910  unibrsiga  32054  eulerpartlemt  32238  eulerpartgbij  32239  ballotlemrinv  32400  hgt750lem2  32532  bnj1146  32671  bnj893  32808  bnj1234  32893  subfacp1lem1  33041  kur14lem2  33069  kur14lem5  33072  kur14lem7  33074  cvmscld  33135  satfv1lem  33224  fmla0  33244  mvtval  33362  mthmpps  33444  riotarab  33575  ttrclresv  33703  noextend  33796  nosupbday  33835  nosupbnd1  33844  nosupbnd2  33846  noinfbday  33850  noinfbnd1  33859  dmscut  33932  madeval2  33964  negs0s  34051  fixun  34138  bj-inrab  35042  bj-inrab3  35044  bj-gabeqis  35053  bj-pr1un  35120  bj-pr2un  35134  bj-dfid2ALT  35163  bj-mpomptALT  35217  rnmptsn  35433  f1omptsnlem  35434  rabiun  35677  phpreu  35688  poimirlem18  35722  ovoliunnfl  35746  voliunnfl  35748  mbfposadd  35751  asindmre  35787  abeqin  36319  rncnvepres  36366  qsresid  36387  rnxrn  36451  xrnres  36455  xrnres2  36456  xrnres3  36457  rncossdmcoss  36500  1cosscnvxrn  36520  refrelsredund4  36672  cdleme25cv  38299  sn-iotalemcor  40118  sqdeccom12  40238  nn0expgcd  40256  sn-00idlem2  40303  sn-1ticom  40337  mendsca  40930  areaquad  40963  cnvrcl0  41122  sqrtcvallem1  41128  trclrelexplem  41208  df3o2  41523  df3o3  41524  cbvmpo2  42536  cbvmpo1  42537  mptssid  42674  fprodabs2  43026  stoweidlem13  43444  wallispilem4  43499  fourierdlem94  43631  fourierdlem102  43639  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fourierdlem114  43651  41prothprmlem2  44958  2exp340mod341  45073  8exp8mod9  45076  nfermltl8rev  45082  cbvmpox2  45559  dmmpossx2  45560  zlmodzxzequa  45725  zlmodzxzequap  45728