Theorem 3eqtr4i 2772

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

Syntax hints:   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  rabbiiaOLD  3437  cbvrabv  3443  rabrab  3457  cbvrabw  3470  cbvrabwOLD  3471  cbvrab  3476  cbvcsbw  3917  cbvcsb  3918  cbvcsbv  3919  csbcow  3922  csbco  3923  cbvrabcsfw  3951  cbvrabcsf  3955  un4  4184  incom  4216  in13  4238  in31  4239  in4  4241  symdifcom  4259  indifcom  4288  indir  4291  undir  4292  indifdir  4300  difdif2  4301  notrab  4327  dfnul3  4342  dfif5  4546  rabsnifsb  4726  prcom  4736  tprot  4753  tpcoma  4754  tpcomb  4755  tpass  4756  qdassr  4758  pw0  4816  pwpw0  4817  pwsn  4904  cbviun  5040  cbviin  5041  cbviung  5042  cbviing  5043  cbviunv  5044  cbviinv  5045  iunrab  5056  iunin1  5076  iinuni  5102  cbvopab  5219  cbvopabv  5220  cbvopab1  5222  cbvopab1g  5223  cbvopab2  5224  cbvopab1s  5225  cbvopab1v  5226  cbvopab2v  5228  unopab  5229  cbvmptf  5256  cbvmptfg  5257  cbvmptv  5260  iunopab  5568  iunopabOLD  5569  dfid4  5583  dfid2  5584  dfid3  5585  rabxp  5736  fconstmpt  5750  csbxp  5787  inxpOLD  5845  cnvco  5898  csbdm  5910  rnmpt  5970  csbres  6002  resundi  6013  resundir  6014  resindi  6015  resindir  6016  rescom  6022  resima  6034  imadmrn  6089  cnvimarndm  6102  cnvi  6163  cnvin  6166  rnun  6167  imaundi  6171  cnvxp  6178  imainrect  6202  csbrn  6224  imacnvcnv  6227  resdmres  6253  imadmres  6255  resdifdir  6258  mptpreima  6259  dfpred3  6333  predin  6349  predun  6350  preddif  6351  frpoind  6364  wfiOLD  6373  cbviotaw  6522  cbviotavw  6523  cbviota  6524  sb8iota  6526  resdif  6869  opabiotadm  6989  fndmin  7064  fninfp  7193  cbvriotaw  7396  cbvriotavw  7397  cbvriota  7400  riotarab  7429  dfoprab2  7490  cbvoprab1  7519  cbvoprab2  7520  cbvoprab12  7521  cbvoprab12v  7522  cbvoprab3  7523  cbvoprab3v  7524  cbvmpox  7525  cbvmpov  7527  resoprab  7550  caov32  7659  caov31  7661  caov4  7663  caovlem2  7668  uniuni  7780  zfrep6  7977  ofmres  8007  dfopab2  8075  dfxp3  8084  dmmpossx  8089  fmpox  8090  fsplit  8140  ovtpos  8264  tposco  8280  frrlem5  8313  tfrlem10  8425  o2p2e4  8577  0map0sn0  8923  mapsncnv  8931  cbvixp  8952  cbvixpv  8953  xpcomco  9100  sbthlem6  9126  1sdomOLD  9282  ttrclresv  9754  frind  9787  cardf2  9980  alephcard  10107  alephfplem1  10141  xp2dju  10214  djuassen  10216  infdju1  10227  pwdju1  10228  ackbij1lem14  10269  compsscnv  10408  dffin1-5  10425  ituniiun  10459  axdc2lem  10485  axdc3lem4  10490  axcclem  10494  pwcfsdom  10620  dmaddpi  10927  dmmulpi  10928  adderpqlem  10991  addassnq  10995  mulcanenq  10997  addcmpblnr  11106  mulcmpblnrlem  11107  ltsrpr  11114  mulgt0sr  11142  sqgt0sr  11143  axi2m1  11196  negiso  12245  nummac  12775  decsubi  12793  9t11e99  12860  fztpval  13622  seqval  14049  sqrecii  14218  sqdivi  14220  binom2i  14247  4bc2eq6  14364  hashgval  14368  revs1  14799  cats1cat  14896  trclublem  15030  shftdm  15106  shftidt2  15116  cji  15194  cbvsum  15727  cbvsumv  15728  sumfc  15741  ackbijnn  15860  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  prodfc  15977  fsumcube  16092  divalglem2  16428  nn0expgcd  16597  nn0gcdsq  16785  prmreclem2  16950  prmrec  16955  hashbc0  17038  dec5nprm  17099  dec2nprm  17100  gcdi  17106  decexp2  17108  decsplit  17116  1259lem1  17164  1259lem4  17167  4001lem1  17174  phlstr  17391  oduval  18344  oduleval  18345  odubas  18347  odubasOLD  18348  lubdm  18408  glbdm  18421  oppgid  19389  symgbas0  19420  gsumcom2  20007  ringidval  20200  oppr1  20366  dfrhm2  20490  rmodislmod  20944  rmodislmodOLD  20945  cnfldsub  21427  cnflddiv  21430  cnflddivOLD  21431  dvdsrzring  21489  pjdm  21744  pjfval2  21746  opsrtoslem1  22096  restco  23187  ufprim  23932  tgioo3  24840  oprpiece1res1  24995  oprpiece1res2  24996  volfiniun  25595  vitalilem4  25659  cbvitg  25825  cbvitgv  25826  itgresr  25828  cbvditg  25903  plyid  26262  coeidp  26317  dgrid  26318  sincos3rdpi  26573  logblog  26849  ang180lem2  26867  1cubrlem  26898  asin1  26951  log2ublem2  27004  log2ublem3  27005  emcllem5  27057  lgsdir2lem5  27387  lgsquadlem3  27440  2lgslem1b  27450  2lgsoddprmlem3d  27471  noextend  27725  nosupbday  27764  nosupbnd1  27773  nosupbnd2  27775  noinfbday  27779  noinfbnd1  27788  dmscut  27870  madeval2  27906  negs0s  28072  negs1s  28073  1p1e2s  28414  cchhllem  28915  cchhllemOLD  28916  ax5seglem7  28964  vtxval0  29070  iedgval0  29071  finsumvtxdg2ssteplem1  29577  wwlksnfi  29935  1wlkdlem1  30165  ex-un  30452  ex-pw  30457  ex-cnv  30465  ex-co  30466  bafval  30632  vsfval  30661  cnnvba  30707  cnnvm  30710  ip2dii  30872  siilem1  30879  h2hcau  31007  hvsubsub4i  31087  hvnegdii  31090  normlem3  31140  normlem8  31145  norm-iii-i  31167  normpar2i  31184  polid2i  31185  chjassi  31514  chj4i  31551  h1de2i  31581  spanunsni  31607  fh3i  31651  fh4i  31652  qlax4i  31658  qlaxr3i  31664  3oalem5  31694  pjadjii  31702  pjsubii  31706  hoadd32i  31806  cnvadj  31920  hh0oi  31931  hhcno  31932  hhcnf  31933  nmopnegi  31993  lnophmlem2  32045  branmfn  32133  dmrab  32524  3unrab  32530  abrexexd  32536  cbviunf  32575  maprnin  32748  dpmul10  32861  dpexpp1  32874  dpadd3  32878  dpmul  32879  dpmul4  32880  psgnfzto1st  33107  cycpmconjs  33158  fracbas  33286  lmlimxrge0  33908  zrhre  33981  qqhre  33982  rrhre  33983  cbvesum  34022  cbvesumv  34023  unibrsiga  34166  eulerpartlemt  34352  eulerpartgbij  34353  ballotlemrinv  34514  hgt750lem2  34645  bnj1146  34783  bnj893  34920  bnj1234  35005  subfacp1lem1  35163  kur14lem2  35191  kur14lem5  35194  kur14lem7  35196  cvmscld  35257  satfv1lem  35346  fmla0  35366  mvtval  35484  mthmpps  35566  fixun  35890  rabeqbii  36175  iuneq12i  36176  iineq1i  36177  iineq12i  36178  riotaeqbii  36179  ixpeq1i  36181  sumeq2si  36183  prodeq2si  36185  itgeq12i  36187  ditgeq123i  36190  cbvcsbvw2  36213  cbviunvw2  36214  cbviinvw2  36215  cbvmptvw2  36216  cbvriotavw2  36218  cbvoprab1vw  36219  cbvoprab2vw  36220  cbvoprab123vw  36221  cbvoprab23vw  36222  cbvoprab13vw  36223  cbvmpovw2  36224  cbvmpo1vw2  36225  cbvmpo2vw2  36226  cbvixpvw2  36227  cbvprodvw2  36229  cbvitgvw2  36230  cbvditgvw2  36231  bj-inrab  36909  bj-inrab3  36911  bj-gabeqis  36920  bj-pr1un  36985  bj-pr2un  36999  bj-dfid2ALT  37047  bj-mpomptALT  37101  rnmptsn  37317  f1omptsnlem  37318  rabiun  37579  phpreu  37590  poimirlem18  37624  ovoliunnfl  37648  voliunnfl  37650  mbfposadd  37653  asindmre  37689  abeqin  38233  rncnvepres  38284  qsresid  38306  rnxrn  38379  xrnres  38383  xrnres2  38384  xrnres3  38385  rncossdmcoss  38436  1cosscnvxrn  38456  refrelsredund4  38613  mpets  38823  cdleme25cv  40340  sn-iotalemcor  42239  sqdeccom12  42302  sumcubes  42325  sn-00idlem2  42405  sn-1ticom  42440  mendsca  43173  areaquad  43204  onsucrn  43260  df3o2  43302  df3o3  43303  omcl3g  43323  dfno2  43417  cnvrcl0  43614  sqrtcvallem1  43620  trclrelexplem  43700  iuneq1i  45024  cbvmpo2  45036  cbvmpo1  45037  cbvrabv2w  45067  mptssid  45184  fprodabs2  45550  stoweidlem13  45968  wallispilem4  46023  fourierdlem94  46155  fourierdlem102  46163  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fourierdlem114  46175  41prothprmlem2  47542  2exp340mod341  47657  8exp8mod9  47660  nfermltl8rev  47666  stgr1  47863  cbvmpox2  48180  dmmpossx2  48181  zlmodzxzequa  48341  zlmodzxzequap  48344