Theorem 3eqtr4i 2854

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  rabrab  3379  rabbiia  3472  cbvrabw  3489  cbvrab  3490  cbvrabv  3491  cbvcsbw  3893  cbvcsb  3894  csbcow  3898  csbco  3899  cbvrabcsfw  3924  cbvrabcsf  3928  un4  4145  incom  4178  in13  4199  in31  4200  in4  4202  symdifcom  4220  indifcom  4249  indir  4252  undir  4253  difdif2  4261  notrab  4280  dfnul3  4295  dfif5  4483  rabsnifsb  4658  prcom  4668  tprot  4685  tpcoma  4686  tpcomb  4687  tpass  4688  qdassr  4690  pw0  4745  pwpw0  4746  pwsn  4830  pwsnOLD  4831  cbviun  4961  cbviin  4962  cbviung  4963  cbviing  4964  iunrab  4976  iunin1  4994  iinuni  5020  cbvopab  5137  cbvopab1  5139  cbvopab1g  5140  cbvopab2  5141  cbvopab1s  5142  cbvopab2v  5144  unopab  5145  cbvmptf  5165  cbvmptfg  5166  iunopab  5446  dfid4  5461  dfid3  5462  rabxp  5600  fconstmpt  5614  csbxp  5650  inxp  5703  cnvco  5756  csbdm  5766  rnmpt  5827  csbres  5856  resundi  5867  resundir  5868  resindi  5869  resindir  5870  rescom  5879  resima  5887  imadmrn  5939  cnvimarndm  5950  cnvi  6000  cnvin  6003  rnun  6004  imaundi  6008  cnvxp  6014  imainrect  6038  csbrn  6060  imacnvcnv  6063  resdmres  6089  imadmres  6091  mptpreima  6092  dfpred3  6158  predin  6171  predun  6172  preddif  6173  wfi  6181  cbviotaw  6321  cbviota  6323  sb8iota  6325  resdif  6635  opabiotadm  6745  fndmin  6815  fninfp  6936  cbvriotaw  7123  cbvriota  7127  dfoprab2  7212  cbvoprab1  7241  cbvoprab2  7242  cbvoprab12  7243  cbvoprab3  7245  cbvmpox  7247  resoprab  7270  caov32  7375  caov31  7377  caov4  7379  caovlem2  7384  uniuni  7484  zfrep6  7656  ofmres  7685  dfopab2  7750  dfxp3  7759  dmmpossx  7764  fmpox  7765  fsplit  7812  fsplitOLD  7813  ovtpos  7907  tposco  7923  tfrlem10  8023  o2p2e4  8166  o2p2e4OLD  8167  0map0sn0  8449  mapsncnv  8457  cbvixp  8478  xpcomco  8607  sbthlem6  8632  1sdom  8721  cardf2  9372  alephcard  9496  alephfplem1  9530  xp2dju  9602  djuassen  9604  infdju1  9615  pwdju1  9616  ackbij1lem14  9655  compsscnv  9793  dffin1-5  9810  ituniiun  9844  axdc2lem  9870  axdc3lem4  9875  axcclem  9879  pwcfsdom  10005  dmaddpi  10312  dmmulpi  10313  adderpqlem  10376  addassnq  10380  mulcanenq  10382  addcmpblnr  10491  mulcmpblnrlem  10492  ltsrpr  10499  mulgt0sr  10527  sqgt0sr  10528  axi2m1  10581  negiso  11621  nummac  12144  decsubi  12162  9t11e99  12229  fztpval  12970  seqval  13381  sqrecii  13547  sqdivi  13549  binom2i  13575  4bc2eq6  13690  hashgval  13694  revs1  14127  cats1cat  14223  trclublem  14355  shftdm  14430  shftidt2  14440  cji  14518  cbvsum  15052  sumfc  15066  ackbijnn  15183  cbvprod  15269  prodfc  15299  fsumcube  15414  divalglem2  15746  nn0gcdsq  16092  prmreclem2  16253  prmrec  16258  hashbc0  16341  dec5nprm  16402  dec2nprm  16403  gcdi  16409  decexp2  16411  decsplit  16419  1259lem1  16464  1259lem4  16467  4001lem1  16474  phlstr  16653  lubdm  17589  glbdm  17602  oduval  17740  oduleval  17741  odubas  17743  oppgid  18484  symgbas0  18517  gsumcom2  19095  ringidval  19253  oppr1  19384  dfrhm2  19469  rmodislmod  19702  opsrtoslem1  20264  cnfldsub  20573  cnflddiv  20575  dvdsrzring  20630  pjdm  20851  pjfval2  20853  restco  21772  ufprim  22517  tgioo3  23413  oprpiece1res1  23555  oprpiece1res2  23556  volfiniun  24148  vitalilem4  24212  cbvitg  24376  itgresr  24379  cbvditg  24452  plyid  24799  coeidp  24853  dgrid  24854  sincos3rdpi  25102  logblog  25370  ang180lem2  25388  1cubrlem  25419  asin1  25472  log2ublem2  25525  log2ublem3  25526  emcllem5  25577  lgsdir2lem5  25905  lgsquadlem3  25958  2lgslem1b  25968  2lgsoddprmlem3d  25989  cchhllem  26673  ax5seglem7  26721  vtxval0  26824  iedgval0  26825  finsumvtxdg2ssteplem1  27327  wwlksnfi  27684  1wlkdlem1  27916  ex-un  28203  ex-pw  28208  ex-cnv  28216  ex-co  28217  bafval  28381  vsfval  28410  cnnvba  28456  cnnvm  28459  ip2dii  28621  siilem1  28628  h2hcau  28756  hvsubsub4i  28836  hvnegdii  28839  normlem3  28889  normlem8  28894  norm-iii-i  28916  normpar2i  28933  polid2i  28934  chjassi  29263  chj4i  29300  h1de2i  29330  spanunsni  29356  fh3i  29400  fh4i  29401  qlax4i  29407  qlaxr3i  29413  3oalem5  29443  pjadjii  29451  pjsubii  29455  hoadd32i  29555  cnvadj  29669  hh0oi  29680  hhcno  29681  hhcnf  29682  nmopnegi  29742  lnophmlem2  29794  branmfn  29882  dmrab  30260  abrexexd  30269  cbviunf  30307  maprnin  30467  dpmul10  30571  dpexpp1  30584  dpadd3  30588  dpmul  30589  dpmul4  30590  psgnfzto1st  30747  cycpmconjs  30798  lmlimxrge0  31191  zrhre  31260  qqhre  31261  rrhre  31262  cbvesum  31301  unibrsiga  31445  eulerpartlemt  31629  eulerpartgbij  31630  ballotlemrinv  31791  hgt750lem2  31923  bnj1146  32063  bnj893  32200  bnj1234  32285  subfacp1lem1  32426  kur14lem2  32454  kur14lem5  32457  kur14lem7  32459  cvmscld  32520  satfv1lem  32609  fmla0  32629  mvtval  32747  mthmpps  32829  frpoind  33080  frind  33085  frrlem5  33127  noextend  33173  nosupbday  33205  nosupbnd1  33214  nosupbnd2  33216  dmscut  33272  madeval2  33290  fixun  33370  bj-inrab  34248  bj-inrab3  34250  bj-pr1un  34318  bj-pr2un  34332  bj-mpomptALT  34414  rnmptsn  34619  f1omptsnlem  34620  rabiun  34880  phpreu  34891  poimirlem18  34925  ovoliunnfl  34949  voliunnfl  34951  mbfposadd  34954  asindmre  34992  abeqin  35529  rncnvepres  35576  qsresid  35597  rnxrn  35661  xrnres  35665  xrnres2  35666  xrnres3  35667  rncossdmcoss  35710  1cosscnvxrn  35730  refrelsredund4  35882  cdleme25cv  37509  sqdeccom12  39195  nn0expgcd  39204  sn-00idlem2  39249  mendsca  39809  areaquad  39843  cnvrcl0  40005  trclrelexplem  40076  df3o2  40394  df3o3  40395  cbvmpo2  41383  cbvmpo1  41384  mptssid  41531  fprodabs2  41896  stoweidlem13  42318  wallispilem4  42373  fourierdlem94  42505  fourierdlem102  42513  fourierdlem111  42522  fourierdlem112  42523  fourierdlem113  42524  fourierdlem114  42525  41prothprmlem2  43803  2exp340mod341  43918  8exp8mod9  43921  nfermltl8rev  43927  cbvmpox2  44404  dmmpossx2  44405  zlmodzxzequa  44571  zlmodzxzequap  44574