Theorem 3eqtr4i 2777

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  rabrab  3312  rabbiia  3408  cbvrabw  3425  cbvrab  3426  cbvrabv  3427  cbvcsbw  3843  cbvcsb  3844  csbcow  3848  csbco  3849  cbvrabcsfw  3877  cbvrabcsf  3881  un4  4104  incom  4136  in13  4157  in31  4158  in4  4160  symdifcom  4178  indifcom  4207  indir  4210  undir  4211  indifdir  4219  difdif2  4221  notrab  4246  dfnul3  4261  dfnul3OLD  4263  dfif5  4476  rabsnifsb  4659  prcom  4669  tprot  4686  tpcoma  4687  tpcomb  4688  tpass  4689  qdassr  4691  pw0  4746  pwpw0  4747  pwsn  4832  pwsnOLD  4833  cbviun  4967  cbviin  4968  cbviung  4969  cbviing  4970  iunrab  4983  iunin1  5002  iinuni  5028  cbvopab  5147  cbvopabv  5148  cbvopab1  5150  cbvopab1g  5151  cbvopab2  5152  cbvopab1s  5153  cbvopab1v  5154  cbvopab2v  5156  unopab  5157  cbvmptf  5184  cbvmptfg  5185  cbvmptv  5188  iunopab  5473  iunopabOLD  5474  dfid4  5491  dfid2  5492  dfid3  5493  rabxp  5636  fconstmpt  5650  csbxp  5687  inxp  5744  cnvco  5797  csbdm  5809  rnmpt  5867  csbres  5897  resundi  5908  resundir  5909  resindi  5910  resindir  5911  rescom  5920  resima  5928  imadmrn  5982  cnvimarndm  5993  cnvi  6050  cnvin  6053  rnun  6054  imaundi  6058  cnvxp  6065  imainrect  6089  csbrn  6111  imacnvcnv  6114  resdmres  6140  imadmres  6142  resdifdir  6145  mptpreima  6146  dfpred3  6217  predin  6234  predun  6235  preddif  6236  frpoind  6249  wfiOLD  6258  cbviotaw  6402  cbviotavw  6403  cbviota  6405  sb8iota  6407  resdif  6746  opabiotadm  6859  fndmin  6931  fninfp  7055  cbvriotaw  7250  cbvriotavw  7251  cbvriota  7255  dfoprab2  7342  cbvoprab1  7371  cbvoprab2  7372  cbvoprab12  7373  cbvoprab3  7375  cbvmpox  7377  resoprab  7401  caov32  7508  caov31  7510  caov4  7512  caovlem2  7517  uniuni  7621  zfrep6  7806  ofmres  7836  dfopab2  7901  dfxp3  7910  dmmpossx  7915  fmpox  7916  fsplit  7966  fsplitOLD  7967  ovtpos  8066  tposco  8082  frrlem5  8115  tfrlem10  8227  o2p2e4  8380  o2p2e4OLD  8381  0map0sn0  8682  mapsncnv  8690  cbvixp  8711  xpcomco  8858  sbthlem6  8884  1sdom  9034  ttrclresv  9484  frind  9517  cardf2  9710  alephcard  9835  alephfplem1  9869  xp2dju  9941  djuassen  9943  infdju1  9954  pwdju1  9955  ackbij1lem14  9998  compsscnv  10136  dffin1-5  10153  ituniiun  10187  axdc2lem  10213  axdc3lem4  10218  axcclem  10222  pwcfsdom  10348  dmaddpi  10655  dmmulpi  10656  adderpqlem  10719  addassnq  10723  mulcanenq  10725  addcmpblnr  10834  mulcmpblnrlem  10835  ltsrpr  10842  mulgt0sr  10870  sqgt0sr  10871  axi2m1  10924  negiso  11964  nummac  12491  decsubi  12509  9t11e99  12576  fztpval  13327  seqval  13741  sqrecii  13909  sqdivi  13911  binom2i  13937  4bc2eq6  14052  hashgval  14056  revs1  14487  cats1cat  14583  trclublem  14715  shftdm  14791  shftidt2  14801  cji  14879  cbvsum  15416  sumfc  15430  ackbijnn  15549  cbvprod  15634  prodfc  15664  fsumcube  15779  divalglem2  16113  nn0gcdsq  16465  prmreclem2  16627  prmrec  16632  hashbc0  16715  dec5nprm  16776  dec2nprm  16777  gcdi  16783  decexp2  16785  decsplit  16793  1259lem1  16841  1259lem4  16844  4001lem1  16851  phlstr  17065  oduval  18015  oduleval  18016  odubas  18018  odubasOLD  18019  lubdm  18078  glbdm  18091  oppgid  18972  symgbas0  19005  gsumcom2  19585  ringidval  19748  oppr1  19885  dfrhm2  19970  rmodislmod  20200  rmodislmodOLD  20201  cnfldsub  20635  cnflddiv  20637  dvdsrzring  20692  pjdm  20923  pjfval2  20925  opsrtoslem1  21271  restco  22324  ufprim  23069  tgioo3  23977  oprpiece1res1  24123  oprpiece1res2  24124  volfiniun  24720  vitalilem4  24784  cbvitg  24949  itgresr  24952  cbvditg  25027  plyid  25379  coeidp  25433  dgrid  25434  sincos3rdpi  25682  logblog  25951  ang180lem2  25969  1cubrlem  26000  asin1  26053  log2ublem2  26106  log2ublem3  26107  emcllem5  26158  lgsdir2lem5  26486  lgsquadlem3  26539  2lgslem1b  26549  2lgsoddprmlem3d  26570  cchhllem  27263  cchhllemOLD  27264  ax5seglem7  27312  vtxval0  27418  iedgval0  27419  finsumvtxdg2ssteplem1  27921  wwlksnfi  28280  1wlkdlem1  28510  ex-un  28797  ex-pw  28802  ex-cnv  28810  ex-co  28811  bafval  28975  vsfval  29004  cnnvba  29050  cnnvm  29053  ip2dii  29215  siilem1  29222  h2hcau  29350  hvsubsub4i  29430  hvnegdii  29433  normlem3  29483  normlem8  29488  norm-iii-i  29510  normpar2i  29527  polid2i  29528  chjassi  29857  chj4i  29894  h1de2i  29924  spanunsni  29950  fh3i  29994  fh4i  29995  qlax4i  30001  qlaxr3i  30007  3oalem5  30037  pjadjii  30045  pjsubii  30049  hoadd32i  30149  cnvadj  30263  hh0oi  30274  hhcno  30275  hhcnf  30276  nmopnegi  30336  lnophmlem2  30388  branmfn  30476  dmrab  30853  abrexexd  30863  cbviunf  30904  maprnin  31075  dpmul10  31178  dpexpp1  31191  dpadd3  31195  dpmul  31196  dpmul4  31197  psgnfzto1st  31381  cycpmconjs  31432  lmlimxrge0  31907  zrhre  31978  qqhre  31979  rrhre  31980  cbvesum  32019  unibrsiga  32163  eulerpartlemt  32347  eulerpartgbij  32348  ballotlemrinv  32509  hgt750lem2  32641  bnj1146  32780  bnj893  32917  bnj1234  33002  subfacp1lem1  33150  kur14lem2  33178  kur14lem5  33181  kur14lem7  33183  cvmscld  33244  satfv1lem  33333  fmla0  33353  mvtval  33471  mthmpps  33553  riotarab  33682  noextend  33878  nosupbday  33917  nosupbnd1  33926  nosupbnd2  33928  noinfbday  33932  noinfbnd1  33941  dmscut  34014  madeval2  34046  negs0s  34133  fixun  34220  bj-inrab  35124  bj-inrab3  35126  bj-gabeqis  35135  bj-pr1un  35202  bj-pr2un  35216  bj-dfid2ALT  35245  bj-mpomptALT  35299  rnmptsn  35515  f1omptsnlem  35516  rabiun  35759  phpreu  35770  poimirlem18  35804  ovoliunnfl  35828  voliunnfl  35830  mbfposadd  35833  asindmre  35869  abeqin  36400  rncnvepres  36446  qsresid  36467  rnxrn  36531  xrnres  36535  xrnres2  36536  xrnres3  36537  rncossdmcoss  36580  1cosscnvxrn  36600  refrelsredund4  36752  cdleme25cv  38379  sn-iotalemcor  40197  sqdeccom12  40324  nn0expgcd  40342  sn-00idlem2  40389  sn-1ticom  40423  mendsca  41021  areaquad  41054  cnvrcl0  41240  sqrtcvallem1  41246  trclrelexplem  41326  df3o2  41641  df3o3  41642  cbvmpo2  42654  cbvmpo1  42655  mptssid  42792  fprodabs2  43143  stoweidlem13  43561  wallispilem4  43616  fourierdlem94  43748  fourierdlem102  43756  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fourierdlem114  43768  41prothprmlem2  45081  2exp340mod341  45196  8exp8mod9  45199  nfermltl8rev  45205  cbvmpox2  45682  dmmpossx2  45683  zlmodzxzequa  45848  zlmodzxzequap  45851