Theorem 3eqtr4i 2796

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  cbvrabv  3425  cbvrabw  3449  cbvrab  3452  cbvcsbw  3860  cbvcsb  3861  cbvcsbv  3862  csbcow  3865  csbco  3866  cbvrabcsfw  3891  cbvrabcsf  3895  incom  4108  in13  4129  in31  4130  in4  4132  un4  4175  symdifcom  4201  indifcom  4230  indir  4233  undir  4234  indifdir  4242  difdif2  4243  notrab  4269  dfnul3  4284  dfif5  4501  rabsnifsb  4682  prcom  4692  tprot  4709  tpcoma  4710  tpcomb  4711  tpass  4712  qdassr  4714  pwsn  4829  pw0  4832  pwpw0  4833  cbviun  4995  cbviin  4996  cbviung  4997  cbviing  4998  cbviunv  4999  cbviinv  5000  iunrab  5013  iunin1  5032  iinuni  5060  cbvopab  5179  cbvopabv  5180  cbvopab1  5181  cbvopab1g  5182  cbvopab2  5183  cbvopab1s  5184  cbvopab1v  5185  cbvopab2v  5186  unopab  5187  cbvmptf  5207  cbvmptfg  5208  cbvmptv  5211  iunopab  5537  dfid4  5550  dfid2  5551  dfid3  5552  rabxp  5702  fconstmpt  5716  csbxp  5756  cnvi  5867  cnvco  5871  csbdm  5883  rnmpt  5943  csbres  5977  resundi  5988  resundir  5989  resindi  5990  resindir  5991  rescom  5997  resima  6061  imadmrnOLD  6073  cnvimarndmOLD  6086  cnvin  6140  rnun  6141  imaundi  6146  cnvxpOLD  6153  imainrect  6178  csbrn  6210  imacnvcnv  6213  resdmres  6239  imadmres  6241  resdifdir  6244  mptpreima  6245  dfpred3  6321  predin  6336  predun  6337  preddif  6338  frpoind  6351  cbviotaw  6507  cbviotavw  6508  cbviota  6509  sb8iota  6511  resdif  6854  opabiotadm  6974  fndmin  7052  fninfp  7186  cbvriotaw  7393  cbvriotavw  7394  cbvriota  7397  riotarab  7426  dfoprab2  7485  cbvoprab1  7514  cbvoprab2  7515  cbvoprab12  7516  cbvoprab12v  7517  cbvoprab3  7518  cbvoprab3v  7519  cbvmpox  7520  cbvmpov  7522  resoprab  7545  caov32  7655  caov31  7657  caov4  7659  caovlem2  7664  mpt3mpt  7692  uniuni  7783  zfrep6OLD  7974  ofmres  8003  dfopab2  8071  dfxp3  8080  dmmpossx  8085  fmpox  8086  fsplit  8138  ovtpos  8269  tposco  8285  frrlem5  8319  tfrlem10  8406  o2p2e4  8560  0map0sn0  8924  mapsncnv  8932  cbvixp  8953  cbvixpv  8954  xpcomco  9097  sbthlem6  9122  ttrclresv  9728  frind  9764  cardf2  10034  alephcard  10159  alephfplem1  10193  xp2dju  10265  djuassen  10267  infdju1  10278  pwdju1  10279  ackbij1lem14  10320  compsscnv  10459  dffin1-5  10476  ituniiun  10510  axdc2lem  10536  axdc3lem4  10541  axcclem  10545  pwcfsdom  10678  dmaddpi  10985  dmmulpi  10986  adderpqlem  11049  addassnq  11053  mulcanenq  11055  addcmpblnr  11164  mulcmpblnrlem  11165  ltsrpr  11172  mulgt0sr  11200  sqgt0sr  11201  axi2m1  11254  negiso  12307  nummac  12874  decsubi  12892  9t11e99OLD  12960  fztpval  13730  seqval  14165  sqrecii  14336  sqdivi  14338  binom2i  14366  4bc2eq6  14483  hashgval  14487  revs1  14925  cats1cat  15023  trclublem  15160  shftdm  15236  shftidt2  15246  cji  15338  cbvsum  15874  cbvsumv  15875  sumfc  15887  ackbijnn  16009  cbvprod  16094  cbvprodv  16095  prodeq1i  16097  prodfc  16124  fsumcube  16238  divalglem2  16577  nn0expgcd  16750  nn0gcdsq  16940  prmrec  17112  hashbc0  17195  dec5nprm  17256  dec2nprm  17257  gcdi  17263  decsplit  17272  1259lem1  17321  1259lem4  17324  4001lem1  17331  phlstr  17529  oduval  18474  oduleval  18475  odubas  18477  lubdm  18535  glbdm  18548  degenmgmopdm  19146  degenmgm2opdm  19150  oppgid  19582  symgbas0  19615  gsumcom2  20201  ringidval  20421  oppr1  20592  dfrhm2  20716  rmodislmod  21217  cnfldsub  21718  cnflddiv  21720  dvdsrzring  21779  pjdm  22025  pjfval2  22027  opsrtoslem1  22376  restco  23494  ufprim  24240  tgioo3  25137  oprpiece1res1  25284  oprpiece1res2  25285  volfiniun  25880  vitalilem4  25944  cbvitg  26108  cbvitgv  26109  itgresr  26111  cbvditg  26186  plyid  26539  coeidp  26594  dgrid  26595  sincos3rdpi  26857  logblog  27132  ang180lem2  27150  1cubrlem  27181  asin1  27234  log2ublem2  27287  log2ublem3  27288  emcllem5  27339  lgsdir2lem5  27668  lgsquadlem3  27721  2lgslem1b  27731  2lgsoddprmlem3d  27752  noextend  28035  nosupbday  28074  nosupbnd1  28083  nosupbnd2  28085  noinfbday  28089  noinfbnd1  28098  dmcuts  28189  madeval2  28231  neg0s  28424  neg1s  28425  cchhllem  29476  ax5seglem7  29525  vtxval0  29629  iedgval0  29630  finsumvtxdg2ssteplem1  30138  wwlksnfi  30507  1wlkdlem1  30740  ex-un  31037  ex-pw  31042  ex-cnv  31050  ex-co  31051  bafval  31218  vsfval  31247  cnnvba  31293  cnnvm  31296  ip2dii  31458  siilem1  31465  h2hcau  31593  hvsubsub4i  31673  hvnegdii  31676  normlem3  31726  normlem8  31731  norm-iii-i  31753  normpar2i  31770  polid2i  31771  chjassi  32100  chj4i  32137  h1de2i  32167  spanunsni  32193  fh3i  32237  fh4i  32238  qlax4i  32244  qlaxr3i  32250  3oalem5  32280  pjadjii  32288  pjsubii  32292  hoadd32i  32392  cnvadj  32506  hh0oi  32517  hhcno  32518  hhcnf  32519  nmopnegi  32579  lnophmlem2  32631  branmfn  32719  dmrab  33147  3unrab  33153  abrexexd  33159  cbviunf  33204  maprnin  33376  dpmul10  33514  dpexpp1  33527  dpadd3  33531  dpmul  33532  dpmul4  33533  psgnfzto1st  33719  cycpmconjs  33770  fracbas  33920  cos9thpiminplylem5  34471  lmlimxrge0  34633  zrhre  34704  qqhre  34705  rrhre  34706  cbvesum  34727  cbvesumv  34728  unibrsiga  34872  eulerpartlemt  35056  eulerpartgbij  35057  ballotlemrinv  35219  hgt750lem2  35334  bnj1146  35474  bnj893  35611  bnj1234  35696  r11  35786  r12  35787  dfk12  35966  dfk22  35967  dfk32  35968  subfacp1lem1  36065  kur14lem2  36093  kur14lem5  36096  kur14lem7  36098  cvmscld  36159  satfv1lem  36248  fmla0  36268  mvtval  36386  mthmpps  36468  fixun  36798  rabeqbii  37110  iuneq12i  37111  iineq1i  37112  iineq12i  37113  riotaeqbii  37114  ixpeq1i  37116  sumeq2si  37118  prodeq2si  37120  itgeq12i  37122  ditgeq123i  37125  cbvcsbvw2  37147  cbviunvw2  37148  cbviinvw2  37149  cbvmptvw2  37150  cbvriotavw2  37152  cbvoprab1vw  37153  cbvoprab2vw  37154  cbvoprab123vw  37155  cbvoprab23vw  37156  cbvoprab13vw  37157  cbvmpovw2  37158  cbvmpo1vw2  37159  cbvmpo2vw2  37160  cbvixpvw2  37161  cbvprodvw2  37163  cbvitgvw2  37164  cbvditgvw2  37165  ttcun  37427  ttciun  37429  bj-inrab  37967  bj-inrab3  37969  bj-gabeqis  37978  bj-pr1un  38043  bj-pr2un  38057  coi1res  38099  bj-dfid2ALT  38119  bj-mpomptALT  38180  rnmptsn  38398  f1omptsnlem  38399  rabiun  38661  phpreu  38667  poimirlem18  38696  ovoliunnfl  38720  voliunnfl  38722  mbfposadd  38725  asindmre  38761  abeqin  39326  rncnvepres  39381  qsresid  39403  dmxrn  39459  rnxrn  39493  xrnres  39497  xrnres2  39498  xrnres3  39499  dmxrncnvepres2  39505  dfsucmap3  39535  dfsucmap2  39536  rncossdmcoss  39617  1cosscnvxrn  39637  refrelsredund4  39788  mpets  40028  dfpetparts2  40044  dfpeters2  40046  petseq  40048  pets2eq  40049  cdleme25cv  41555  sn-iotalemcor  43416  sqdeccom12  43486  sumcubes  43510  resuppsinopn  43554  sn-00idlem2  43590  sn-1ticom  43626  mendsca  44327  areaquad  44358  onsucrn  44413  df3o2  44455  df3o3  44456  omcl3g  44476  dfno2  44569  cnvrcl0  44765  sqrtcvallem1  44771  trclrelexplem  44851  k0004val0  45294  iuneq1i  46240  cbvmpo2  46251  cbvmpo1  46252  cbvrabv2w  46282  mptssid  46392  fprodabs2  46746  stoweidlem13  47162  wallispilem4  47217  fourierdlem94  47349  fourierdlem102  47357  fourierdlem111  47366  fourierdlem112  47367  fourierdlem113  47368  fourierdlem114  47369  41prothprmlem2  48842  2exp340mod341  48970  8exp8mod9  48973  nfermltl8rev  48979  stgr1  49198  gpgprismgr4cycllem6  49337  gpgprismgr4cycllem9  49340  gpgprismgr4cycllem10  49341  cbvmpox2  49587  dmmpossx2  49588  zlmodzxzequa  49747  zlmodzxzequap  49750  2sphere  50000  resinsn  50124  dfswapf2  50522