Theorem 3eqtr4i 2798

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  cbvrabv  3428  cbvrabw  3453  cbvrab  3456  cbvcsbw  3864  cbvcsb  3865  cbvcsbv  3866  csbcow  3869  csbco  3870  cbvrabcsfw  3895  cbvrabcsf  3899  un4  4128  incom  4162  in13  4183  in31  4184  in4  4186  symdifcom  4207  indifcom  4236  indir  4239  undir  4240  indifdir  4248  difdif2  4249  notrab  4275  dfnul3  4290  dfif5  4506  rabsnifsb  4690  prcom  4700  tprot  4717  tpcoma  4718  tpcomb  4719  tpass  4720  qdassr  4722  pw0  4780  pwpw0  4781  pwsn  4867  cbviun  5001  cbviin  5002  cbviung  5003  cbviing  5004  cbviunv  5005  cbviinv  5006  iunrab  5019  iunin1  5038  iinuni  5066  cbvopab  5185  cbvopabv  5186  cbvopab1  5187  cbvopab1g  5188  cbvopab2  5189  cbvopab1s  5190  cbvopab1v  5191  cbvopab2v  5192  unopab  5193  cbvmptf  5213  cbvmptfg  5214  cbvmptv  5217  iunopab  5546  dfid4  5559  dfid2  5560  dfid3  5561  rabxp  5711  fconstmpt  5725  csbxp  5764  cnvi  5873  cnvco  5877  csbdm  5889  rnmpt  5949  csbres  5983  resundi  5994  resundir  5995  resindi  5996  resindir  5997  rescom  6003  resima  6016  imadmrn  6074  cnvimarndm  6087  cnvin  6143  rnun  6144  imaundi  6149  cnvxp  6156  imainrect  6181  csbrn  6206  imacnvcnv  6209  resdmres  6235  imadmres  6237  resdifdir  6240  mptpreima  6241  dfpred3  6317  predin  6332  predun  6333  preddif  6334  frpoind  6347  cbviotaw  6503  cbviotavw  6504  cbviota  6505  sb8iota  6507  resdif  6846  opabiotadm  6966  fndmin  7044  fninfp  7178  cbvriotaw  7385  cbvriotavw  7386  cbvriota  7389  riotarab  7418  dfoprab2  7477  cbvoprab1  7506  cbvoprab2  7507  cbvoprab12  7508  cbvoprab12v  7509  cbvoprab3  7510  cbvoprab3v  7511  cbvmpox  7512  cbvmpov  7514  resoprab  7537  caov32  7647  caov31  7649  caov4  7651  caovlem2  7656  uniuni  7767  zfrep6OLD  7958  ofmres  7987  dfopab2  8055  dfxp3  8064  dmmpossx  8069  fmpox  8070  fsplit  8118  ovtpos  8243  tposco  8259  frrlem5  8293  tfrlem10  8380  o2p2e4  8532  0map0sn0  8889  mapsncnv  8897  cbvixp  8918  cbvixpv  8919  xpcomco  9062  sbthlem6  9087  ttrclresv  9693  frind  9729  cardf2  9945  alephcard  10070  alephfplem1  10104  xp2dju  10176  djuassen  10178  infdju1  10189  pwdju1  10190  ackbij1lem14  10231  compsscnv  10370  dffin1-5  10387  ituniiun  10421  axdc2lem  10447  axdc3lem4  10452  axcclem  10456  pwcfsdom  10585  dmaddpi  10892  dmmulpi  10893  adderpqlem  10956  addassnq  10960  mulcanenq  10962  addcmpblnr  11071  mulcmpblnrlem  11072  ltsrpr  11079  mulgt0sr  11107  sqgt0sr  11108  axi2m1  11161  negiso  12212  nummac  12779  decsubi  12797  9t11e99OLD  12865  fztpval  13633  seqval  14068  sqrecii  14239  sqdivi  14241  binom2i  14268  4bc2eq6  14385  hashgval  14389  revs1  14826  cats1cat  14924  trclublem  15058  shftdm  15134  shftidt2  15144  cji  15236  cbvsum  15772  cbvsumv  15773  sumfc  15785  ackbijnn  15907  cbvprod  15992  cbvprodv  15993  prodeq1i  15995  prodfc  16024  fsumcube  16138  divalglem2  16477  nn0expgcd  16646  nn0gcdsq  16835  prmreclem2  17001  prmrec  17006  hashbc0  17089  dec5nprm  17150  dec2nprm  17151  gcdi  17157  decsplit  17166  1259lem1  17215  1259lem4  17218  4001lem1  17225  phlstr  17423  oduval  18368  oduleval  18369  odubas  18371  lubdm  18429  glbdm  18442  degenmgmopdm  19036  degenmgm2opdm  19040  oppgid  19472  symgbas0  19505  gsumcom2  20091  ringidval  20311  oppr1  20480  dfrhm2  20604  rmodislmod  21103  cnfldsub  21602  cnflddiv  21604  dvdsrzring  21663  pjdm  21909  pjfval2  21911  opsrtoslem1  22258  restco  23373  ufprim  24119  tgioo3  25016  oprpiece1res1  25163  oprpiece1res2  25164  volfiniun  25759  vitalilem4  25823  cbvitg  25988  cbvitgv  25989  itgresr  25991  cbvditg  26066  plyid  26419  coeidp  26473  dgrid  26474  sincos3rdpi  26735  logblog  27010  ang180lem2  27028  1cubrlem  27059  asin1  27112  log2ublem2  27165  log2ublem3  27166  emcllem5  27217  lgsdir2lem5  27546  lgsquadlem3  27599  2lgslem1b  27609  2lgsoddprmlem3d  27630  noextend  27883  nosupbday  27922  nosupbnd1  27931  nosupbnd2  27933  noinfbday  27937  noinfbnd1  27946  dmcuts  28037  madeval2  28079  neg0s  28272  neg1s  28273  cchhllem  29293  ax5seglem7  29342  vtxval0  29446  iedgval0  29447  finsumvtxdg2ssteplem1  29955  wwlksnfi  30324  1wlkdlem1  30557  ex-un  30848  ex-pw  30853  ex-cnv  30861  ex-co  30862  bafval  31029  vsfval  31058  cnnvba  31104  cnnvm  31107  ip2dii  31269  siilem1  31276  h2hcau  31404  hvsubsub4i  31484  hvnegdii  31487  normlem3  31537  normlem8  31542  norm-iii-i  31564  normpar2i  31581  polid2i  31582  chjassi  31911  chj4i  31948  h1de2i  31978  spanunsni  32004  fh3i  32048  fh4i  32049  qlax4i  32055  qlaxr3i  32061  3oalem5  32091  pjadjii  32099  pjsubii  32103  hoadd32i  32203  cnvadj  32317  hh0oi  32328  hhcno  32329  hhcnf  32330  nmopnegi  32390  lnophmlem2  32442  branmfn  32530  dmrab  32916  3unrab  32922  abrexexd  32928  cbviunf  32973  maprnin  33148  dpmul10  33286  dpexpp1  33299  dpadd3  33303  dpmul  33304  dpmul4  33305  psgnfzto1st  33491  cycpmconjs  33542  fracbas  33692  cos9thpiminplylem5  34242  lmlimxrge0  34404  zrhre  34475  qqhre  34476  rrhre  34477  cbvesum  34498  cbvesumv  34499  unibrsiga  34643  eulerpartlemt  34828  eulerpartgbij  34829  ballotlemrinv  34991  hgt750lem2  35106  bnj1146  35246  bnj893  35383  bnj1234  35468  r11  35547  r12  35548  subfacp1lem1  35710  kur14lem2  35738  kur14lem5  35741  kur14lem7  35743  cvmscld  35804  satfv1lem  35893  fmla0  35913  mvtval  36031  mthmpps  36113  fixun  36438  rabeqbii  36765  iuneq12i  36766  iineq1i  36767  iineq12i  36768  riotaeqbii  36769  ixpeq1i  36771  sumeq2si  36773  prodeq2si  36775  itgeq12i  36777  ditgeq123i  36780  cbvcsbvw2  36802  cbviunvw2  36803  cbviinvw2  36804  cbvmptvw2  36805  cbvriotavw2  36807  cbvoprab1vw  36808  cbvoprab2vw  36809  cbvoprab123vw  36810  cbvoprab23vw  36811  cbvoprab13vw  36812  cbvmpovw2  36813  cbvmpo1vw2  36814  cbvmpo2vw2  36815  cbvixpvw2  36816  cbvprodvw2  36818  cbvitgvw2  36819  cbvditgvw2  36820  ttcun  37082  ttciun  37084  bj-inrab  37622  bj-inrab3  37624  bj-gabeqis  37633  bj-pr1un  37698  bj-pr2un  37712  bj-dfid2ALT  37760  bj-mpomptALT  37820  rnmptsn  38040  f1omptsnlem  38041  rabiun  38303  phpreu  38314  poimirlem18  38348  ovoliunnfl  38372  voliunnfl  38374  mbfposadd  38377  asindmre  38413  abeqin  38963  rncnvepres  39018  qsresid  39040  dmxrn  39096  rnxrn  39130  xrnres  39134  xrnres2  39135  xrnres3  39136  dmxrncnvepres2  39142  dfsucmap3  39172  dfsucmap2  39173  rncossdmcoss  39254  1cosscnvxrn  39274  refrelsredund4  39425  mpets  39665  dfpetparts2  39681  dfpeters2  39683  petseq  39685  pets2eq  39686  cdleme25cv  41192  sn-iotalemcor  43053  sqdeccom12  43110  sumcubes  43134  resuppsinopn  43184  sn-00idlem2  43220  sn-1ticom  43256  mendsca  43972  areaquad  44003  onsucrn  44058  df3o2  44100  df3o3  44101  omcl3g  44121  dfno2  44214  cnvrcl0  44411  sqrtcvallem1  44417  trclrelexplem  44497  iuneq1i  45864  cbvmpo2  45875  cbvmpo1  45876  cbvrabv2w  45906  mptssid  46016  fprodabs2  46371  stoweidlem13  46787  wallispilem4  46842  fourierdlem94  46974  fourierdlem102  46982  fourierdlem111  46991  fourierdlem112  46992  fourierdlem113  46993  fourierdlem114  46994  41prothprmlem2  48430  2exp340mod341  48558  8exp8mod9  48561  nfermltl8rev  48567  stgr1  48786  gpgprismgr4cycllem6  48925  gpgprismgr4cycllem9  48928  gpgprismgr4cycllem10  48929  cbvmpox2  49175  dmmpossx2  49176  zlmodzxzequa  49335  zlmodzxzequap  49338  resinsn  49709  dfswapf2  50098