Theorem 3eqtr4i 2791

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

Syntax hints:   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750

This theorem is referenced by:  rabrab  3297  rabbiia  3384  cbvrabw  3402  cbvrab  3403  cbvrabv  3404  cbvcsbw  3817  cbvcsb  3818  csbcow  3822  csbco  3823  cbvrabcsfw  3848  cbvrabcsf  3852  un4  4076  incom  4108  in13  4129  in31  4130  in4  4132  symdifcom  4150  indifcom  4179  indir  4182  undir  4183  indifdir  4191  difdif2  4193  notrab  4216  dfnul3  4230  dfif5  4439  rabsnifsb  4618  prcom  4628  tprot  4645  tpcoma  4646  tpcomb  4647  tpass  4648  qdassr  4650  pw0  4705  pwpw0  4706  pwsn  4793  pwsnOLD  4794  cbviun  4928  cbviin  4929  cbviung  4930  cbviing  4931  iunrab  4944  iunin1  4963  iinuni  4989  cbvopab  5107  cbvopab1  5109  cbvopab1g  5110  cbvopab2  5111  cbvopab1s  5112  cbvopab2v  5114  unopab  5115  cbvmptf  5135  cbvmptfg  5136  iunopab  5420  dfid4  5435  dfid3  5436  rabxp  5574  fconstmpt  5588  csbxp  5624  inxp  5678  cnvco  5731  csbdm  5743  rnmpt  5801  csbres  5831  resundi  5842  resundir  5843  resindi  5844  resindir  5845  rescom  5854  resima  5862  imadmrn  5916  cnvimarndm  5927  cnvi  5977  cnvin  5980  rnun  5981  imaundi  5985  cnvxp  5991  imainrect  6015  csbrn  6037  imacnvcnv  6040  resdmres  6066  imadmres  6068  resdifdir  6071  mptpreima  6072  dfpred3  6141  predin  6154  predun  6155  preddif  6156  wfi  6164  cbviotaw  6306  cbviota  6308  sb8iota  6310  resdif  6627  opabiotadm  6739  fndmin  6811  fninfp  6933  cbvriotaw  7123  cbvriota  7127  dfoprab2  7212  cbvoprab1  7241  cbvoprab2  7242  cbvoprab12  7243  cbvoprab3  7245  cbvmpox  7247  resoprab  7270  caov32  7377  caov31  7379  caov4  7381  caovlem2  7386  uniuni  7489  zfrep6  7666  ofmres  7695  dfopab2  7760  dfxp3  7769  dmmpossx  7774  fmpox  7775  fsplit  7823  fsplitOLD  7824  ovtpos  7923  tposco  7939  tfrlem10  8039  o2p2e4  8182  o2p2e4OLD  8183  0map0sn0  8480  mapsncnv  8488  cbvixp  8509  xpcomco  8641  sbthlem6  8667  1sdom  8772  cardf2  9418  alephcard  9543  alephfplem1  9577  xp2dju  9649  djuassen  9651  infdju1  9662  pwdju1  9663  ackbij1lem14  9706  compsscnv  9844  dffin1-5  9861  ituniiun  9895  axdc2lem  9921  axdc3lem4  9926  axcclem  9930  pwcfsdom  10056  dmaddpi  10363  dmmulpi  10364  adderpqlem  10427  addassnq  10431  mulcanenq  10433  addcmpblnr  10542  mulcmpblnrlem  10543  ltsrpr  10550  mulgt0sr  10578  sqgt0sr  10579  axi2m1  10632  negiso  11670  nummac  12195  decsubi  12213  9t11e99  12280  fztpval  13031  seqval  13442  sqrecii  13609  sqdivi  13611  binom2i  13637  4bc2eq6  13752  hashgval  13756  revs1  14187  cats1cat  14283  trclublem  14415  shftdm  14491  shftidt2  14501  cji  14579  cbvsum  15113  sumfc  15127  ackbijnn  15244  cbvprod  15330  prodfc  15360  fsumcube  15475  divalglem2  15809  nn0gcdsq  16160  prmreclem2  16321  prmrec  16326  hashbc0  16409  dec5nprm  16470  dec2nprm  16471  gcdi  16477  decexp2  16479  decsplit  16487  1259lem1  16535  1259lem4  16538  4001lem1  16545  phlstr  16724  lubdm  17668  glbdm  17681  oduval  17819  oduleval  17820  odubas  17822  oppgid  18564  symgbas0  18597  gsumcom2  19176  ringidval  19334  oppr1  19468  dfrhm2  19553  rmodislmod  19783  cnfldsub  20207  cnflddiv  20209  dvdsrzring  20264  pjdm  20485  pjfval2  20487  opsrtoslem1  20828  restco  21877  ufprim  22622  tgioo3  23519  oprpiece1res1  23665  oprpiece1res2  23666  volfiniun  24260  vitalilem4  24324  cbvitg  24488  itgresr  24491  cbvditg  24566  plyid  24918  coeidp  24972  dgrid  24973  sincos3rdpi  25221  logblog  25490  ang180lem2  25508  1cubrlem  25539  asin1  25592  log2ublem2  25645  log2ublem3  25646  emcllem5  25697  lgsdir2lem5  26025  lgsquadlem3  26078  2lgslem1b  26088  2lgsoddprmlem3d  26109  cchhllem  26793  ax5seglem7  26841  vtxval0  26944  iedgval0  26945  finsumvtxdg2ssteplem1  27447  wwlksnfi  27804  1wlkdlem1  28034  ex-un  28321  ex-pw  28326  ex-cnv  28334  ex-co  28335  bafval  28499  vsfval  28528  cnnvba  28574  cnnvm  28577  ip2dii  28739  siilem1  28746  h2hcau  28874  hvsubsub4i  28954  hvnegdii  28957  normlem3  29007  normlem8  29012  norm-iii-i  29034  normpar2i  29051  polid2i  29052  chjassi  29381  chj4i  29418  h1de2i  29448  spanunsni  29474  fh3i  29518  fh4i  29519  qlax4i  29525  qlaxr3i  29531  3oalem5  29561  pjadjii  29569  pjsubii  29573  hoadd32i  29673  cnvadj  29787  hh0oi  29798  hhcno  29799  hhcnf  29800  nmopnegi  29860  lnophmlem2  29912  branmfn  30000  dmrab  30379  abrexexd  30389  cbviunf  30430  maprnin  30602  dpmul10  30705  dpexpp1  30718  dpadd3  30722  dpmul  30723  dpmul4  30724  psgnfzto1st  30910  cycpmconjs  30961  lmlimxrge0  31431  zrhre  31500  qqhre  31501  rrhre  31502  cbvesum  31541  unibrsiga  31685  eulerpartlemt  31869  eulerpartgbij  31870  ballotlemrinv  32031  hgt750lem2  32163  bnj1146  32303  bnj893  32440  bnj1234  32525  subfacp1lem1  32669  kur14lem2  32697  kur14lem5  32700  kur14lem7  32702  cvmscld  32763  satfv1lem  32852  fmla0  32872  mvtval  32990  mthmpps  33072  riotarab  33203  frpoind  33339  frind  33347  frrlem5  33401  noextend  33466  nosupbday  33505  nosupbnd1  33514  nosupbnd2  33516  noinfbday  33520  noinfbnd1  33529  dmscut  33600  madeval2  33631  negs0s  33707  fixun  33794  bj-inrab  34684  bj-inrab3  34686  bj-pr1un  34754  bj-pr2un  34768  bj-mpomptALT  34848  rnmptsn  35066  f1omptsnlem  35067  rabiun  35344  phpreu  35355  poimirlem18  35389  ovoliunnfl  35413  voliunnfl  35415  mbfposadd  35418  asindmre  35454  abeqin  35988  rncnvepres  36035  qsresid  36056  rnxrn  36120  xrnres  36124  xrnres2  36125  xrnres3  36126  rncossdmcoss  36169  1cosscnvxrn  36189  refrelsredund4  36341  cdleme25cv  37968  sqdeccom12  39854  nn0expgcd  39867  sn-00idlem2  39914  sn-1ticom  39948  mendsca  40541  areaquad  40574  cnvrcl0  40733  sqrtcvallem1  40739  trclrelexplem  40820  df3o2  41135  df3o3  41136  cbvmpo2  42141  cbvmpo1  42142  mptssid  42280  fprodabs2  42638  stoweidlem13  43056  wallispilem4  43111  fourierdlem94  43243  fourierdlem102  43251  fourierdlem111  43260  fourierdlem112  43261  fourierdlem113  43262  fourierdlem114  43263  41prothprmlem2  44552  2exp340mod341  44667  8exp8mod9  44670  nfermltl8rev  44676  cbvmpox2  45153  dmmpossx2  45154  zlmodzxzequa  45319  zlmodzxzequap  45322