Theorem 3eqtr4i 2768

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 2761	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2761	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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  rabbiiaOLD  3435  cbvrabv  3440  rabrab  3453  cbvrabw  3465  cbvrab  3471  cbvcsbw  3902  cbvcsb  3903  csbcow  3907  csbco  3908  cbvrabcsfw  3936  cbvrabcsf  3940  un4  4168  incom  4200  in13  4221  in31  4222  in4  4224  symdifcom  4242  indifcom  4271  indir  4274  undir  4275  indifdir  4283  difdif2  4285  notrab  4310  dfnul3  4325  dfnul3OLD  4327  dfif5  4543  rabsnifsb  4725  prcom  4735  tprot  4752  tpcoma  4753  tpcomb  4754  tpass  4755  qdassr  4757  pw0  4814  pwpw0  4815  pwsn  4899  pwsnOLD  4900  cbviun  5038  cbviin  5039  cbviung  5040  cbviing  5041  iunrab  5054  iunin1  5074  iinuni  5100  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  5558  iunopabOLD  5559  dfid4  5574  dfid2  5575  dfid3  5576  rabxp  5723  fconstmpt  5737  csbxp  5774  inxp  5831  cnvco  5884  csbdm  5896  rnmpt  5953  csbres  5983  resundi  5994  resundir  5995  resindi  5996  resindir  5997  rescom  6006  resima  6014  imadmrn  6068  cnvimarndm  6080  cnvi  6140  cnvin  6143  rnun  6144  imaundi  6148  cnvxp  6155  imainrect  6179  csbrn  6201  imacnvcnv  6204  resdmres  6230  imadmres  6232  resdifdir  6235  mptpreima  6236  dfpred3  6310  predin  6327  predun  6328  preddif  6329  frpoind  6342  wfiOLD  6351  cbviotaw  6501  cbviotavw  6502  cbviota  6504  sb8iota  6506  resdif  6853  opabiotadm  6972  fndmin  7045  fninfp  7173  cbvriotaw  7376  cbvriotavw  7377  cbvriota  7381  riotarab  7410  dfoprab2  7469  cbvoprab1  7498  cbvoprab2  7499  cbvoprab12  7500  cbvoprab3  7502  cbvmpox  7504  resoprab  7528  caov32  7636  caov31  7638  caov4  7640  caovlem2  7645  uniuni  7751  zfrep6  7943  ofmres  7973  dfopab2  8040  dfxp3  8049  dmmpossx  8054  fmpox  8055  fsplit  8105  ovtpos  8228  tposco  8244  frrlem5  8277  tfrlem10  8389  o2p2e4  8543  0map0sn0  8881  mapsncnv  8889  cbvixp  8910  xpcomco  9064  sbthlem6  9090  1sdomOLD  9251  ttrclresv  9714  frind  9747  cardf2  9940  alephcard  10067  alephfplem1  10101  xp2dju  10173  djuassen  10175  infdju1  10186  pwdju1  10187  ackbij1lem14  10230  compsscnv  10368  dffin1-5  10385  ituniiun  10419  axdc2lem  10445  axdc3lem4  10450  axcclem  10454  pwcfsdom  10580  dmaddpi  10887  dmmulpi  10888  adderpqlem  10951  addassnq  10955  mulcanenq  10957  addcmpblnr  11066  mulcmpblnrlem  11067  ltsrpr  11074  mulgt0sr  11102  sqgt0sr  11103  axi2m1  11156  negiso  12198  nummac  12726  decsubi  12744  9t11e99  12811  fztpval  13567  seqval  13981  sqrecii  14151  sqdivi  14153  binom2i  14180  4bc2eq6  14293  hashgval  14297  revs1  14719  cats1cat  14816  trclublem  14946  shftdm  15022  shftidt2  15032  cji  15110  cbvsum  15645  sumfc  15659  ackbijnn  15778  cbvprod  15863  prodfc  15893  fsumcube  16008  divalglem2  16342  nn0gcdsq  16692  prmreclem2  16854  prmrec  16859  hashbc0  16942  dec5nprm  17003  dec2nprm  17004  gcdi  17010  decexp2  17012  decsplit  17020  1259lem1  17068  1259lem4  17071  4001lem1  17078  phlstr  17295  oduval  18245  oduleval  18246  odubas  18248  odubasOLD  18249  lubdm  18308  glbdm  18321  oppgid  19264  symgbas0  19297  gsumcom2  19884  ringidval  20077  oppr1  20241  dfrhm2  20365  rmodislmod  20684  rmodislmodOLD  20685  cnfldsub  21173  cnflddiv  21175  dvdsrzring  21232  pjdm  21481  pjfval2  21483  opsrtoslem1  21835  restco  22888  ufprim  23633  tgioo3  24541  oprpiece1res1  24696  oprpiece1res2  24697  volfiniun  25296  vitalilem4  25360  cbvitg  25525  itgresr  25528  cbvditg  25603  plyid  25958  coeidp  26013  dgrid  26014  sincos3rdpi  26262  logblog  26533  ang180lem2  26551  1cubrlem  26582  asin1  26635  log2ublem2  26688  log2ublem3  26689  emcllem5  26740  lgsdir2lem5  27068  lgsquadlem3  27121  2lgslem1b  27131  2lgsoddprmlem3d  27152  noextend  27405  nosupbday  27444  nosupbnd1  27453  nosupbnd2  27455  noinfbday  27459  noinfbnd1  27468  dmscut  27549  madeval2  27585  negs0s  27740  cchhllem  28411  cchhllemOLD  28412  ax5seglem7  28460  vtxval0  28566  iedgval0  28567  finsumvtxdg2ssteplem1  29069  wwlksnfi  29427  1wlkdlem1  29657  ex-un  29944  ex-pw  29949  ex-cnv  29957  ex-co  29958  bafval  30124  vsfval  30153  cnnvba  30199  cnnvm  30202  ip2dii  30364  siilem1  30371  h2hcau  30499  hvsubsub4i  30579  hvnegdii  30582  normlem3  30632  normlem8  30637  norm-iii-i  30659  normpar2i  30676  polid2i  30677  chjassi  31006  chj4i  31043  h1de2i  31073  spanunsni  31099  fh3i  31143  fh4i  31144  qlax4i  31150  qlaxr3i  31156  3oalem5  31186  pjadjii  31194  pjsubii  31198  hoadd32i  31298  cnvadj  31412  hh0oi  31423  hhcno  31424  hhcnf  31425  nmopnegi  31485  lnophmlem2  31537  branmfn  31625  dmrab  32004  abrexexd  32013  cbviunf  32054  maprnin  32223  dpmul10  32328  dpexpp1  32341  dpadd3  32345  dpmul  32346  dpmul4  32347  psgnfzto1st  32534  cycpmconjs  32585  lmlimxrge0  33226  zrhre  33297  qqhre  33298  rrhre  33299  cbvesum  33338  unibrsiga  33482  eulerpartlemt  33668  eulerpartgbij  33669  ballotlemrinv  33830  hgt750lem2  33962  bnj1146  34100  bnj893  34237  bnj1234  34322  subfacp1lem1  34468  kur14lem2  34496  kur14lem5  34499  kur14lem7  34501  cvmscld  34562  satfv1lem  34651  fmla0  34671  mvtval  34789  mthmpps  34871  fixun  35185  bj-inrab  36110  bj-inrab3  36112  bj-gabeqis  36121  bj-pr1un  36187  bj-pr2un  36201  bj-dfid2ALT  36249  bj-mpomptALT  36303  rnmptsn  36519  f1omptsnlem  36520  rabiun  36764  phpreu  36775  poimirlem18  36809  ovoliunnfl  36833  voliunnfl  36835  mbfposadd  36838  asindmre  36874  abeqin  37423  rncnvepres  37475  qsresid  37497  rnxrn  37571  xrnres  37575  xrnres2  37576  xrnres3  37577  rncossdmcoss  37628  1cosscnvxrn  37648  refrelsredund4  37805  mpets  38015  cdleme25cv  39532  sn-iotalemcor  41345  sqdeccom12  41503  sumcubes  41513  nn0expgcd  41528  sn-00idlem2  41574  sn-1ticom  41609  mendsca  42233  areaquad  42267  onsucrn  42323  df3o2  42365  df3o3  42366  omcl3g  42386  dfno2  42481  cnvrcl0  42678  sqrtcvallem1  42684  trclrelexplem  42764  cbvmpo2  44087  cbvmpo1  44088  mptssid  44242  fprodabs2  44609  stoweidlem13  45027  wallispilem4  45082  fourierdlem94  45214  fourierdlem102  45222  fourierdlem111  45231  fourierdlem112  45232  fourierdlem113  45233  fourierdlem114  45234  41prothprmlem2  46584  2exp340mod341  46699  8exp8mod9  46702  nfermltl8rev  46708  cbvmpox2  47099  dmmpossx2  47100  zlmodzxzequa  47264  zlmodzxzequap  47267