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 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  cbvrabv  3401  cbvrabw  3426  cbvrabwOLD  3427  cbvrab  3430  cbvcsbw  3841  cbvcsb  3842  cbvcsbv  3843  csbcow  3846  csbco  3847  cbvrabcsfw  3872  cbvrabcsf  3876  un4  4104  incom  4138  in13  4159  in31  4160  in4  4162  symdifcom  4182  indifcom  4211  indir  4214  undir  4215  indifdir  4223  difdif2  4224  notrab  4250  dfnul3  4265  dfif5  4471  rabsnifsb  4654  prcom  4664  tprot  4681  tpcoma  4682  tpcomb  4683  tpass  4684  qdassr  4686  pw0  4743  pwpw0  4744  pwsn  4831  cbviun  4964  cbviin  4965  cbviung  4966  cbviing  4967  cbviunv  4968  cbviinv  4969  iunrab  4982  iunin1  5001  iinuni  5027  cbvopab  5144  cbvopabv  5145  cbvopab1  5146  cbvopab1g  5147  cbvopab2  5148  cbvopab1s  5149  cbvopab1v  5150  cbvopab2v  5151  unopab  5152  cbvmptf  5172  cbvmptfg  5173  cbvmptv  5176  iunopab  5501  dfid4  5514  dfid2  5515  dfid3  5516  rabxp  5666  fconstmpt  5680  csbxp  5719  cnvco  5827  csbdm  5839  rnmpt  5899  csbres  5934  resundi  5945  resundir  5946  resindi  5947  resindir  5948  rescom  5954  resima  5967  imadmrn  6022  cnvimarndm  6035  cnvi  6092  cnvin  6095  rnun  6096  imaundi  6100  cnvxp  6108  imainrect  6132  csbrn  6154  imacnvcnv  6157  resdmres  6183  imadmres  6185  resdifdir  6188  mptpreima  6189  dfpred3  6263  predin  6278  predun  6279  preddif  6280  frpoind  6293  cbviotaw  6448  cbviotavw  6449  cbviota  6450  sb8iota  6452  resdif  6788  opabiotadm  6908  fndmin  6986  fninfp  7118  cbvriotaw  7322  cbvriotavw  7323  cbvriota  7326  riotarab  7355  dfoprab2  7414  cbvoprab1  7443  cbvoprab2  7444  cbvoprab12  7445  cbvoprab12v  7446  cbvoprab3  7447  cbvoprab3v  7448  cbvmpox  7449  cbvmpov  7451  resoprab  7474  caov32  7583  caov31  7585  caov4  7587  caovlem2  7592  uniuni  7705  zfrep6OLD  7897  ofmres  7926  dfopab2  7994  dfxp3  8003  dmmpossx  8008  fmpox  8009  fsplit  8056  ovtpos  8181  tposco  8197  frrlem5  8230  tfrlem10  8316  o2p2e4  8466  0map0sn0  8823  mapsncnv  8831  cbvixp  8852  cbvixpv  8853  xpcomco  8995  sbthlem6  9020  ttrclresv  9629  frind  9665  cardf2  9858  alephcard  9983  alephfplem1  10017  xp2dju  10090  djuassen  10092  infdju1  10103  pwdju1  10104  ackbij1lem14  10145  compsscnv  10284  dffin1-5  10301  ituniiun  10335  axdc2lem  10361  axdc3lem4  10366  axcclem  10370  pwcfsdom  10497  dmaddpi  10804  dmmulpi  10805  adderpqlem  10868  addassnq  10872  mulcanenq  10874  addcmpblnr  10983  mulcmpblnrlem  10984  ltsrpr  10991  mulgt0sr  11019  sqgt0sr  11020  axi2m1  11073  negiso  12127  nummac  12680  decsubi  12698  9t11e99  12765  fztpval  13531  seqval  13965  sqrecii  14136  sqdivi  14138  binom2i  14165  4bc2eq6  14282  hashgval  14286  revs1  14718  cats1cat  14814  trclublem  14948  shftdm  15024  shftidt2  15034  cji  15112  cbvsum  15648  cbvsumv  15649  sumfc  15662  ackbijnn  15784  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  prodfc  15901  fsumcube  16016  divalglem2  16355  nn0expgcd  16524  nn0gcdsq  16713  prmreclem2  16879  prmrec  16884  hashbc0  16967  dec5nprm  17028  dec2nprm  17029  gcdi  17035  decsplit  17044  1259lem1  17092  1259lem4  17095  4001lem1  17102  phlstr  17300  oduval  18245  oduleval  18246  odubas  18248  lubdm  18306  glbdm  18319  oppgid  19322  symgbas0  19355  gsumcom2  19941  ringidval  20155  oppr1  20321  dfrhm2  20445  rmodislmod  20920  cnfldsub  21375  cnflddiv  21377  dvdsrzring  21436  pjdm  21682  pjfval2  21684  opsrtoslem1  22031  restco  23147  ufprim  23892  tgioo3  24789  oprpiece1res1  24936  oprpiece1res2  24937  volfiniun  25532  vitalilem4  25596  cbvitg  25761  cbvitgv  25762  itgresr  25764  cbvditg  25839  plyid  26192  coeidp  26246  dgrid  26247  sincos3rdpi  26499  logblog  26774  ang180lem2  26792  1cubrlem  26823  asin1  26876  log2ublem2  26929  log2ublem3  26930  emcllem5  26981  lgsdir2lem5  27310  lgsquadlem3  27363  2lgslem1b  27373  2lgsoddprmlem3d  27394  noextend  27648  nosupbday  27687  nosupbnd1  27696  nosupbnd2  27698  noinfbday  27702  noinfbnd1  27711  dmcuts  27801  madeval2  27843  neg0s  28036  neg1s  28037  cchhllem  28973  ax5seglem7  29022  vtxval0  29126  iedgval0  29127  finsumvtxdg2ssteplem1  29632  wwlksnfi  29992  1wlkdlem1  30225  ex-un  30512  ex-pw  30517  ex-cnv  30525  ex-co  30526  bafval  30693  vsfval  30722  cnnvba  30768  cnnvm  30771  ip2dii  30933  siilem1  30940  h2hcau  31068  hvsubsub4i  31148  hvnegdii  31151  normlem3  31201  normlem8  31206  norm-iii-i  31228  normpar2i  31245  polid2i  31246  chjassi  31575  chj4i  31612  h1de2i  31642  spanunsni  31668  fh3i  31712  fh4i  31713  qlax4i  31719  qlaxr3i  31725  3oalem5  31755  pjadjii  31763  pjsubii  31767  hoadd32i  31867  cnvadj  31981  hh0oi  31992  hhcno  31993  hhcnf  31994  nmopnegi  32054  lnophmlem2  32106  branmfn  32194  dmrab  32584  3unrab  32591  abrexexd  32597  cbviunf  32644  maprnin  32823  dpmul10  32973  dpexpp1  32986  dpadd3  32990  dpmul  32991  dpmul4  32992  psgnfzto1st  33186  cycpmconjs  33237  fracbas  33389  cos9thpiminplylem5  33970  lmlimxrge0  34132  zrhre  34203  qqhre  34204  rrhre  34205  cbvesum  34226  cbvesumv  34227  unibrsiga  34370  eulerpartlemt  34555  eulerpartgbij  34556  ballotlemrinv  34718  hgt750lem2  34836  bnj1146  34973  bnj893  35110  bnj1234  35195  r11  35275  r12  35276  subfacp1lem1  35407  kur14lem2  35435  kur14lem5  35438  kur14lem7  35440  cvmscld  35501  satfv1lem  35590  fmla0  35610  mvtval  35728  mthmpps  35810  fixun  36135  rabeqbii  36422  iuneq12i  36423  iineq1i  36424  iineq12i  36425  riotaeqbii  36426  ixpeq1i  36428  sumeq2si  36430  prodeq2si  36432  itgeq12i  36434  ditgeq123i  36437  cbvcsbvw2  36459  cbviunvw2  36460  cbviinvw2  36461  cbvmptvw2  36462  cbvriotavw2  36464  cbvoprab1vw  36465  cbvoprab2vw  36466  cbvoprab123vw  36467  cbvoprab23vw  36468  cbvoprab13vw  36469  cbvmpovw2  36470  cbvmpo1vw2  36471  cbvmpo2vw2  36472  cbvixpvw2  36473  cbvprodvw2  36475  cbvitgvw2  36476  cbvditgvw2  36477  ttcun  36740  ttciun  36742  bj-inrab  37280  bj-inrab3  37282  bj-gabeqis  37291  bj-pr1un  37356  bj-pr2un  37370  bj-dfid2ALT  37418  bj-mpomptALT  37477  rnmptsn  37697  f1omptsnlem  37698  rabiun  37960  phpreu  37971  poimirlem18  38005  ovoliunnfl  38029  voliunnfl  38031  mbfposadd  38034  asindmre  38070  abeqin  38621  rncnvepres  38676  qsresid  38698  dmxrn  38754  rnxrn  38788  xrnres  38792  xrnres2  38793  xrnres3  38794  dmxrncnvepres2  38800  dfsucmap3  38830  dfsucmap2  38831  rncossdmcoss  38912  1cosscnvxrn  38932  refrelsredund4  39083  mpets  39323  dfpetparts2  39339  dfpeters2  39341  petseq  39343  pets2eq  39344  cdleme25cv  40850  sn-iotalemcor  42709  sqdeccom12  42766  sumcubes  42790  resuppsinopn  42840  sn-00idlem2  42876  sn-1ticom  42912  mendsca  43630  areaquad  43661  onsucrn  43716  df3o2  43758  df3o3  43759  omcl3g  43779  dfno2  43872  cnvrcl0  44069  sqrtcvallem1  44075  trclrelexplem  44155  iuneq1i  45532  cbvmpo2  45544  cbvmpo1  45545  cbvrabv2w  45575  mptssid  45685  fprodabs2  46040  stoweidlem13  46456  wallispilem4  46511  fourierdlem94  46643  fourierdlem102  46651  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fourierdlem114  46663  41prothprmlem2  48096  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  stgr1  48452  gpgprismgr4cycllem6  48591  gpgprismgr4cycllem9  48594  gpgprismgr4cycllem10  48595  cbvmpox2  48827  dmmpossx2  48828  zlmodzxzequa  48987  zlmodzxzequap  48990  resinsn  49362  dfswapf2  49751