Theorem 3eqtr4i 2793

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 2786	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2786	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 2155  ax-ext 2732

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

This theorem is used by:  cbvrabv  3422  cbvrabw  3446  cbvrab  3449  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbcow  3862  csbco  3863  cbvrabcsfw  3888  cbvrabcsf  3892  un4  4121  incom  4155  in13  4176  in31  4177  in4  4179  symdifcom  4200  indifcom  4229  indir  4232  undir  4233  indifdir  4241  difdif2  4242  notrab  4268  dfnul3  4283  dfif5  4499  rabsnifsb  4683  prcom  4693  tprot  4710  tpcoma  4711  tpcomb  4712  tpass  4713  qdassr  4715  pw0  4773  pwpw0  4774  pwsn  4860  cbviun  4993  cbviin  4994  cbviung  4995  cbviing  4996  cbviunv  4997  cbviinv  4998  iunrab  5011  iunin1  5030  iinuni  5058  cbvopab  5177  cbvopabv  5178  cbvopab1  5179  cbvopab1g  5180  cbvopab2  5181  cbvopab1s  5182  cbvopab1v  5183  cbvopab2v  5184  unopab  5185  cbvmptf  5205  cbvmptfg  5206  cbvmptv  5209  iunopab  5538  dfid4  5551  dfid2  5552  dfid3  5553  rabxp  5703  fconstmpt  5717  csbxp  5756  cnvi  5865  cnvco  5869  csbdm  5881  rnmpt  5941  csbres  5975  resundi  5986  resundir  5987  resindi  5988  resindir  5989  rescom  5995  resima  6008  imadmrn  6066  cnvimarndm  6079  cnvin  6135  rnun  6136  imaundi  6141  cnvxpOLD  6149  imainrect  6174  csbrn  6199  imacnvcnv  6202  resdmres  6228  imadmres  6230  resdifdir  6233  mptpreima  6234  dfpred3  6310  predin  6325  predun  6326  preddif  6327  frpoind  6340  cbviotaw  6496  cbviotavw  6497  cbviota  6498  sb8iota  6500  resdif  6840  opabiotadm  6960  fndmin  7038  fninfp  7173  cbvriotaw  7380  cbvriotavw  7381  cbvriota  7384  riotarab  7413  dfoprab2  7472  cbvoprab1  7501  cbvoprab2  7502  cbvoprab12  7503  cbvoprab12v  7504  cbvoprab3  7505  cbvoprab3v  7506  cbvmpox  7507  cbvmpov  7509  resoprab  7532  caov32  7642  caov31  7644  caov4  7646  caovlem2  7651  uniuni  7762  zfrep6OLD  7953  ofmres  7982  dfopab2  8050  dfxp3  8059  dmmpossx  8064  fmpox  8065  fsplit  8115  ovtpos  8240  tposco  8256  frrlem5  8290  tfrlem10  8377  o2p2e4  8531  0map0sn0  8895  mapsncnv  8903  cbvixp  8924  cbvixpv  8925  xpcomco  9068  sbthlem6  9093  ttrclresv  9699  frind  9735  cardf2  9951  alephcard  10076  alephfplem1  10110  xp2dju  10182  djuassen  10184  infdju1  10195  pwdju1  10196  ackbij1lem14  10237  compsscnv  10376  dffin1-5  10393  ituniiun  10427  axdc2lem  10453  axdc3lem4  10458  axcclem  10462  pwcfsdom  10595  dmaddpi  10902  dmmulpi  10903  adderpqlem  10966  addassnq  10970  mulcanenq  10972  addcmpblnr  11081  mulcmpblnrlem  11082  ltsrpr  11089  mulgt0sr  11117  sqgt0sr  11118  axi2m1  11171  negiso  12222  nummac  12789  decsubi  12807  9t11e99OLD  12875  fztpval  13644  seqval  14079  sqrecii  14250  sqdivi  14252  binom2i  14279  4bc2eq6  14396  hashgval  14400  revs1  14837  cats1cat  14935  trclublem  15071  shftdm  15147  shftidt2  15157  cji  15249  cbvsum  15785  cbvsumv  15786  sumfc  15798  ackbijnn  15920  cbvprod  16005  cbvprodv  16006  prodeq1i  16008  prodfc  16035  fsumcube  16149  divalglem2  16488  nn0expgcd  16657  nn0gcdsq  16846  prmreclem2  17012  prmrec  17017  hashbc0  17100  dec5nprm  17161  dec2nprm  17162  gcdi  17168  decsplit  17177  1259lem1  17226  1259lem4  17229  4001lem1  17236  phlstr  17434  oduval  18379  oduleval  18380  odubas  18382  lubdm  18440  glbdm  18453  degenmgmopdm  19050  degenmgm2opdm  19054  oppgid  19486  symgbas0  19519  gsumcom2  20105  ringidval  20325  oppr1  20494  dfrhm2  20618  rmodislmod  21117  cnfldsub  21616  cnflddiv  21618  dvdsrzring  21677  pjdm  21923  pjfval2  21925  opsrtoslem1  22274  restco  23392  ufprim  24138  tgioo3  25035  oprpiece1res1  25182  oprpiece1res2  25183  volfiniun  25778  vitalilem4  25842  cbvitg  26006  cbvitgv  26007  itgresr  26009  cbvditg  26084  plyid  26437  coeidp  26492  dgrid  26493  sincos3rdpi  26757  logblog  27032  ang180lem2  27050  1cubrlem  27081  asin1  27134  log2ublem2  27187  log2ublem3  27188  emcllem5  27239  lgsdir2lem5  27568  lgsquadlem3  27621  2lgslem1b  27631  2lgsoddprmlem3d  27652  noextend  27905  nosupbday  27944  nosupbnd1  27953  nosupbnd2  27955  noinfbday  27959  noinfbnd1  27968  dmcuts  28059  madeval2  28101  neg0s  28294  neg1s  28295  cchhllem  29346  ax5seglem7  29395  vtxval0  29499  iedgval0  29500  finsumvtxdg2ssteplem1  30008  wwlksnfi  30377  1wlkdlem1  30610  ex-un  30907  ex-pw  30912  ex-cnv  30920  ex-co  30921  bafval  31088  vsfval  31117  cnnvba  31163  cnnvm  31166  ip2dii  31328  siilem1  31335  h2hcau  31463  hvsubsub4i  31543  hvnegdii  31546  normlem3  31596  normlem8  31601  norm-iii-i  31623  normpar2i  31640  polid2i  31641  chjassi  31970  chj4i  32007  h1de2i  32037  spanunsni  32063  fh3i  32107  fh4i  32108  qlax4i  32114  qlaxr3i  32120  3oalem5  32150  pjadjii  32158  pjsubii  32162  hoadd32i  32262  cnvadj  32376  hh0oi  32387  hhcno  32388  hhcnf  32389  nmopnegi  32449  lnophmlem2  32501  branmfn  32589  dmrab  32975  3unrab  32981  abrexexd  32987  cbviunf  33032  maprnin  33205  dpmul10  33343  dpexpp1  33356  dpadd3  33360  dpmul  33361  dpmul4  33362  psgnfzto1st  33548  cycpmconjs  33599  fracbas  33749  cos9thpiminplylem5  34299  lmlimxrge0  34461  zrhre  34532  qqhre  34533  rrhre  34534  cbvesum  34555  cbvesumv  34556  unibrsiga  34700  eulerpartlemt  34885  eulerpartgbij  34886  ballotlemrinv  35048  hgt750lem2  35163  bnj1146  35303  bnj893  35440  bnj1234  35525  r11  35604  r12  35605  subfacp1lem1  35761  kur14lem2  35789  kur14lem5  35792  kur14lem7  35794  cvmscld  35855  satfv1lem  35944  fmla0  35964  mvtval  36082  mthmpps  36164  fixun  36489  rabeqbii  36817  iuneq12i  36818  iineq1i  36819  iineq12i  36820  riotaeqbii  36821  ixpeq1i  36823  sumeq2si  36825  prodeq2si  36827  itgeq12i  36829  ditgeq123i  36832  cbvcsbvw2  36854  cbviunvw2  36855  cbviinvw2  36856  cbvmptvw2  36857  cbvriotavw2  36859  cbvoprab1vw  36860  cbvoprab2vw  36861  cbvoprab123vw  36862  cbvoprab23vw  36863  cbvoprab13vw  36864  cbvmpovw2  36865  cbvmpo1vw2  36866  cbvmpo2vw2  36867  cbvixpvw2  36868  cbvprodvw2  36870  cbvitgvw2  36871  cbvditgvw2  36872  ttcun  37134  ttciun  37136  bj-inrab  37674  bj-inrab3  37676  bj-gabeqis  37685  bj-pr1un  37750  bj-pr2un  37764  bj-dfid2ALT  37812  bj-mpomptALT  37872  rnmptsn  38092  f1omptsnlem  38093  rabiun  38355  phpreu  38361  poimirlem18  38390  ovoliunnfl  38414  voliunnfl  38416  mbfposadd  38419  asindmre  38455  abeqin  39005  rncnvepres  39060  qsresid  39082  dmxrn  39138  rnxrn  39172  xrnres  39176  xrnres2  39177  xrnres3  39178  dmxrncnvepres2  39184  dfsucmap3  39214  dfsucmap2  39215  rncossdmcoss  39296  1cosscnvxrn  39316  refrelsredund4  39467  mpets  39707  dfpetparts2  39723  dfpeters2  39725  petseq  39727  pets2eq  39728  cdleme25cv  41234  sn-iotalemcor  43095  sqdeccom12  43167  sumcubes  43191  resuppsinopn  43241  sn-00idlem2  43277  sn-1ticom  43313  mendsca  44029  areaquad  44060  onsucrn  44115  df3o2  44157  df3o3  44158  omcl3g  44178  dfno2  44271  cnvrcl0  44468  sqrtcvallem1  44474  trclrelexplem  44554  iuneq1i  45921  cbvmpo2  45932  cbvmpo1  45933  cbvrabv2w  45963  mptssid  46073  fprodabs2  46428  stoweidlem13  46844  wallispilem4  46899  fourierdlem94  47031  fourierdlem102  47039  fourierdlem111  47048  fourierdlem112  47049  fourierdlem113  47050  fourierdlem114  47051  41prothprmlem2  48524  2exp340mod341  48652  8exp8mod9  48655  nfermltl8rev  48661  stgr1  48880  gpgprismgr4cycllem6  49019  gpgprismgr4cycllem9  49022  gpgprismgr4cycllem10  49023  cbvmpox2  49269  dmmpossx2  49270  zlmodzxzequa  49429  zlmodzxzequap  49432  resinsn  49801  dfswapf2  50190