Theorem 3eqtr4i 2795

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  cbvrabv  3424  cbvrabw  3449  cbvrabwOLD  3450  cbvrab  3453  cbvcsbw  3862  cbvcsb  3863  cbvcsbv  3864  csbcow  3867  csbco  3868  cbvrabcsfw  3893  cbvrabcsf  3897  un4  4127  incom  4161  in13  4182  in31  4183  in4  4185  symdifcom  4206  indifcom  4235  indir  4238  undir  4239  indifdir  4247  difdif2  4248  notrab  4274  dfnul3  4289  dfif5  4497  rabsnifsb  4681  prcom  4691  tprot  4708  tpcoma  4709  tpcomb  4710  tpass  4711  qdassr  4713  pw0  4770  pwpw0  4771  pwsn  4858  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iunrab  5010  iunin1  5029  iinuni  5055  cbvopab  5172  cbvopabv  5173  cbvopab1  5174  cbvopab1g  5175  cbvopab2  5176  cbvopab1s  5177  cbvopab1v  5178  cbvopab2v  5179  unopab  5180  cbvmptf  5200  cbvmptfg  5201  cbvmptv  5204  iunopab  5530  dfid4  5543  dfid2  5544  dfid3  5545  rabxp  5695  fconstmpt  5709  csbxp  5748  cnvi  5857  cnvco  5861  csbdm  5873  rnmpt  5933  csbres  5968  resundi  5979  resundir  5980  resindi  5981  resindir  5982  rescom  5988  resima  6001  imadmrn  6059  cnvimarndm  6072  cnvin  6128  rnun  6129  imaundi  6134  cnvxp  6142  imainrect  6167  csbrn  6190  imacnvcnv  6193  resdmres  6219  imadmres  6221  resdifdir  6224  mptpreima  6225  dfpred3  6299  predin  6314  predun  6315  preddif  6316  frpoind  6329  cbviotaw  6484  cbviotavw  6485  cbviota  6486  sb8iota  6488  resdif  6828  opabiotadm  6948  fndmin  7026  fninfp  7158  cbvriotaw  7362  cbvriotavw  7363  cbvriota  7366  riotarab  7395  dfoprab2  7454  cbvoprab1  7483  cbvoprab2  7484  cbvoprab12  7485  cbvoprab12v  7486  cbvoprab3  7487  cbvoprab3v  7488  cbvmpox  7489  cbvmpov  7491  resoprab  7514  caov32  7623  caov31  7625  caov4  7627  caovlem2  7632  uniuni  7745  zfrep6OLD  7936  ofmres  7965  dfopab2  8033  dfxp3  8042  dmmpossx  8047  fmpox  8048  fsplit  8096  ovtpos  8221  tposco  8237  frrlem5  8271  tfrlem10  8358  o2p2e4  8510  0map0sn0  8867  mapsncnv  8875  cbvixp  8896  cbvixpv  8897  xpcomco  9039  sbthlem6  9064  ttrclresv  9672  frind  9708  cardf2  9901  alephcard  10026  alephfplem1  10060  xp2dju  10133  djuassen  10135  infdju1  10146  pwdju1  10147  ackbij1lem14  10188  compsscnv  10328  dffin1-5  10345  ituniiun  10379  axdc2lem  10405  axdc3lem4  10410  axcclem  10414  pwcfsdom  10541  dmaddpi  10848  dmmulpi  10849  adderpqlem  10912  addassnq  10916  mulcanenq  10918  addcmpblnr  11027  mulcmpblnrlem  11028  ltsrpr  11035  mulgt0sr  11063  sqgt0sr  11064  axi2m1  11117  negiso  12172  nummac  12738  decsubi  12756  9t11e99OLD  12824  fztpval  13591  seqval  14025  sqrecii  14196  sqdivi  14198  binom2i  14225  4bc2eq6  14342  hashgval  14346  revs1  14778  cats1cat  14874  trclublem  15008  shftdm  15084  shftidt2  15094  cji  15186  cbvsum  15722  cbvsumv  15723  sumfc  15736  ackbijnn  15858  cbvprod  15943  cbvprodv  15944  prodeq1i  15946  prodfc  15975  fsumcube  16090  divalglem2  16429  nn0expgcd  16598  nn0gcdsq  16787  prmreclem2  16953  prmrec  16958  hashbc0  17041  dec5nprm  17102  dec2nprm  17103  gcdi  17109  decsplit  17118  1259lem1  17167  1259lem4  17170  4001lem1  17177  phlstr  17375  oduval  18320  oduleval  18321  odubas  18323  lubdm  18381  glbdm  18394  oppgid  19396  symgbas0  19429  gsumcom2  20015  ringidval  20233  oppr1  20399  dfrhm2  20523  rmodislmod  20997  cnfldsub  21452  cnflddiv  21454  dvdsrzring  21513  pjdm  21759  pjfval2  21761  opsrtoslem1  22108  restco  23224  ufprim  23969  tgioo3  24866  oprpiece1res1  25013  oprpiece1res2  25014  volfiniun  25609  vitalilem4  25673  cbvitg  25838  cbvitgv  25839  itgresr  25841  cbvditg  25916  plyid  26269  coeidp  26323  dgrid  26324  sincos3rdpi  26582  logblog  26857  ang180lem2  26875  1cubrlem  26906  asin1  26959  log2ublem2  27012  log2ublem3  27013  emcllem5  27064  lgsdir2lem5  27393  lgsquadlem3  27446  2lgslem1b  27456  2lgsoddprmlem3d  27477  noextend  27730  nosupbday  27769  nosupbnd1  27778  nosupbnd2  27780  noinfbday  27784  noinfbnd1  27793  dmcuts  27884  madeval2  27926  neg0s  28119  neg1s  28120  cchhllem  29087  ax5seglem7  29136  vtxval0  29240  iedgval0  29241  finsumvtxdg2ssteplem1  29746  wwlksnfi  30106  1wlkdlem1  30339  ex-un  30626  ex-pw  30631  ex-cnv  30639  ex-co  30640  bafval  30807  vsfval  30836  cnnvba  30882  cnnvm  30885  ip2dii  31047  siilem1  31054  h2hcau  31182  hvsubsub4i  31262  hvnegdii  31265  normlem3  31315  normlem8  31320  norm-iii-i  31342  normpar2i  31359  polid2i  31360  chjassi  31689  chj4i  31726  h1de2i  31756  spanunsni  31782  fh3i  31826  fh4i  31827  qlax4i  31833  qlaxr3i  31839  3oalem5  31869  pjadjii  31877  pjsubii  31881  hoadd32i  31981  cnvadj  32095  hh0oi  32106  hhcno  32107  hhcnf  32108  nmopnegi  32168  lnophmlem2  32220  branmfn  32308  dmrab  32696  3unrab  32702  abrexexd  32708  cbviunf  32755  maprnin  32933  dpmul10  33072  dpexpp1  33085  dpadd3  33089  dpmul  33090  dpmul4  33091  psgnfzto1st  33285  cycpmconjs  33336  fracbas  33492  cos9thpiminplylem5  34083  lmlimxrge0  34245  zrhre  34316  qqhre  34317  rrhre  34318  cbvesum  34339  cbvesumv  34340  unibrsiga  34483  eulerpartlemt  34668  eulerpartgbij  34669  ballotlemrinv  34831  hgt750lem2  34946  bnj1146  35086  bnj893  35223  bnj1234  35308  r11  35390  r12  35391  subfacp1lem1  35529  kur14lem2  35557  kur14lem5  35560  kur14lem7  35562  cvmscld  35623  satfv1lem  35712  fmla0  35732  mvtval  35850  mthmpps  35932  fixun  36257  rabeqbii  36554  iuneq12i  36555  iineq1i  36556  iineq12i  36557  riotaeqbii  36558  ixpeq1i  36560  sumeq2si  36562  prodeq2si  36564  itgeq12i  36566  ditgeq123i  36569  cbvcsbvw2  36591  cbviunvw2  36592  cbviinvw2  36593  cbvmptvw2  36594  cbvriotavw2  36596  cbvoprab1vw  36597  cbvoprab2vw  36598  cbvoprab123vw  36599  cbvoprab23vw  36600  cbvoprab13vw  36601  cbvmpovw2  36602  cbvmpo1vw2  36603  cbvmpo2vw2  36604  cbvixpvw2  36605  cbvprodvw2  36607  cbvitgvw2  36608  cbvditgvw2  36609  ttcun  36872  ttciun  36874  bj-inrab  37412  bj-inrab3  37414  bj-gabeqis  37423  bj-pr1un  37488  bj-pr2un  37502  bj-dfid2ALT  37550  bj-mpomptALT  37609  rnmptsn  37829  f1omptsnlem  37830  rabiun  38092  phpreu  38103  poimirlem18  38137  ovoliunnfl  38161  voliunnfl  38163  mbfposadd  38166  asindmre  38202  abeqin  38753  rncnvepres  38808  qsresid  38830  dmxrn  38886  rnxrn  38920  xrnres  38924  xrnres2  38925  xrnres3  38926  dmxrncnvepres2  38932  dfsucmap3  38962  dfsucmap2  38963  rncossdmcoss  39044  1cosscnvxrn  39064  refrelsredund4  39215  mpets  39455  dfpetparts2  39471  dfpeters2  39473  petseq  39475  pets2eq  39476  cdleme25cv  40982  sn-iotalemcor  42841  sqdeccom12  42898  sumcubes  42922  resuppsinopn  42972  sn-00idlem2  43008  sn-1ticom  43044  mendsca  43762  areaquad  43793  onsucrn  43848  df3o2  43890  df3o3  43891  omcl3g  43911  dfno2  44004  cnvrcl0  44201  sqrtcvallem1  44207  trclrelexplem  44287  iuneq1i  45664  cbvmpo2  45675  cbvmpo1  45676  cbvrabv2w  45706  mptssid  45816  fprodabs2  46171  stoweidlem13  46587  wallispilem4  46642  fourierdlem94  46774  fourierdlem102  46782  fourierdlem111  46791  fourierdlem112  46792  fourierdlem113  46793  fourierdlem114  46794  41prothprmlem2  48227  2exp340mod341  48355  8exp8mod9  48358  nfermltl8rev  48364  stgr1  48583  gpgprismgr4cycllem6  48722  gpgprismgr4cycllem9  48725  gpgprismgr4cycllem10  48726  cbvmpox2  48958  dmmpossx2  48959  zlmodzxzequa  49118  zlmodzxzequap  49121  resinsn  49493  dfswapf2  49882