Theorem 3eqtr4i 2802

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  cbvrabv  3433  cbvrabw  3458  cbvrabwOLD  3459  cbvrab  3462  cbvcsbw  3871  cbvcsb  3872  cbvcsbv  3873  csbcow  3876  csbco  3877  cbvrabcsfw  3902  cbvrabcsf  3906  un4  4136  incom  4170  in13  4191  in31  4192  in4  4194  symdifcom  4215  indifcom  4244  indir  4247  undir  4248  indifdir  4256  difdif2  4257  notrab  4283  dfnul3  4298  dfif5  4509  rabsnifsb  4693  prcom  4703  tprot  4720  tpcoma  4721  tpcomb  4722  tpass  4723  qdassr  4725  pw0  4782  pwpw0  4783  pwsn  4869  cbviun  5003  cbviin  5004  cbviung  5005  cbviing  5006  cbviunv  5007  cbviinv  5008  iunrab  5021  iunin1  5040  iinuni  5068  cbvopab  5187  cbvopabv  5188  cbvopab1  5189  cbvopab1g  5190  cbvopab2  5191  cbvopab1s  5192  cbvopab1v  5193  cbvopab2v  5194  unopab  5195  cbvmptf  5215  cbvmptfg  5216  cbvmptv  5219  iunopab  5545  dfid4  5558  dfid2  5559  dfid3  5560  rabxp  5710  fconstmpt  5724  csbxp  5763  cnvi  5872  cnvco  5876  csbdm  5888  rnmpt  5948  csbres  5982  resundi  5993  resundir  5994  resindi  5995  resindir  5996  rescom  6002  resima  6015  imadmrn  6073  cnvimarndm  6086  cnvin  6142  rnun  6143  imaundi  6148  cnvxp  6155  imainrect  6180  csbrn  6205  imacnvcnv  6208  resdmres  6234  imadmres  6236  resdifdir  6239  mptpreima  6240  dfpred3  6314  predin  6329  predun  6330  preddif  6331  frpoind  6344  cbviotaw  6500  cbviotavw  6501  cbviota  6502  sb8iota  6504  resdif  6843  opabiotadm  6963  fndmin  7041  fninfp  7173  cbvriotaw  7377  cbvriotavw  7378  cbvriota  7381  riotarab  7410  dfoprab2  7469  cbvoprab1  7498  cbvoprab2  7499  cbvoprab12  7500  cbvoprab12v  7501  cbvoprab3  7502  cbvoprab3v  7503  cbvmpox  7504  cbvmpov  7506  resoprab  7529  caov32  7638  caov31  7640  caov4  7642  caovlem2  7647  uniuni  7761  zfrep6OLD  7952  ofmres  7981  dfopab2  8049  dfxp3  8058  dmmpossx  8063  fmpox  8064  fsplit  8112  ovtpos  8237  tposco  8253  frrlem5  8287  tfrlem10  8374  o2p2e4  8526  0map0sn0  8883  mapsncnv  8891  cbvixp  8912  cbvixpv  8913  xpcomco  9055  sbthlem6  9080  ttrclresv  9686  frind  9722  cardf2  9929  alephcard  10054  alephfplem1  10088  xp2dju  10160  djuassen  10162  infdju1  10173  pwdju1  10174  ackbij1lem14  10215  compsscnv  10355  dffin1-5  10372  ituniiun  10406  axdc2lem  10432  axdc3lem4  10437  axcclem  10441  pwcfsdom  10568  dmaddpi  10875  dmmulpi  10876  adderpqlem  10939  addassnq  10943  mulcanenq  10945  addcmpblnr  11054  mulcmpblnrlem  11055  ltsrpr  11062  mulgt0sr  11090  sqgt0sr  11091  axi2m1  11144  negiso  12195  nummac  12761  decsubi  12779  9t11e99OLD  12847  fztpval  13614  seqval  14048  sqrecii  14219  sqdivi  14221  binom2i  14248  4bc2eq6  14365  hashgval  14369  revs1  14802  cats1cat  14898  trclublem  15032  shftdm  15108  shftidt2  15118  cji  15210  cbvsum  15746  cbvsumv  15747  sumfc  15760  ackbijnn  15882  cbvprod  15967  cbvprodv  15968  prodeq1i  15970  prodfc  15999  fsumcube  16114  divalglem2  16453  nn0expgcd  16622  nn0gcdsq  16811  prmreclem2  16977  prmrec  16982  hashbc0  17065  dec5nprm  17126  dec2nprm  17127  gcdi  17133  decsplit  17142  1259lem1  17191  1259lem4  17194  4001lem1  17201  phlstr  17399  oduval  18344  oduleval  18345  odubas  18347  lubdm  18405  glbdm  18418  oppgid  19426  symgbas0  19459  gsumcom2  20045  ringidval  20265  oppr1  20432  dfrhm2  20556  rmodislmod  21029  cnfldsub  21519  cnflddiv  21521  dvdsrzring  21580  pjdm  21826  pjfval2  21828  opsrtoslem1  22175  restco  23290  ufprim  24035  tgioo3  24932  oprpiece1res1  25079  oprpiece1res2  25080  volfiniun  25675  vitalilem4  25739  cbvitg  25904  cbvitgv  25905  itgresr  25907  cbvditg  25982  plyid  26335  coeidp  26389  dgrid  26390  sincos3rdpi  26648  logblog  26923  ang180lem2  26941  1cubrlem  26972  asin1  27025  log2ublem2  27078  log2ublem3  27079  emcllem5  27130  lgsdir2lem5  27459  lgsquadlem3  27512  2lgslem1b  27522  2lgsoddprmlem3d  27543  noextend  27796  nosupbday  27835  nosupbnd1  27844  nosupbnd2  27846  noinfbday  27850  noinfbnd1  27859  dmcuts  27950  madeval2  27992  neg0s  28185  neg1s  28186  cchhllem  29177  ax5seglem7  29226  vtxval0  29330  iedgval0  29331  finsumvtxdg2ssteplem1  29836  wwlksnfi  30196  1wlkdlem1  30429  ex-un  30716  ex-pw  30721  ex-cnv  30729  ex-co  30730  bafval  30897  vsfval  30926  cnnvba  30972  cnnvm  30975  ip2dii  31137  siilem1  31144  h2hcau  31272  hvsubsub4i  31352  hvnegdii  31355  normlem3  31405  normlem8  31410  norm-iii-i  31432  normpar2i  31449  polid2i  31450  chjassi  31779  chj4i  31816  h1de2i  31846  spanunsni  31872  fh3i  31916  fh4i  31917  qlax4i  31923  qlaxr3i  31929  3oalem5  31959  pjadjii  31967  pjsubii  31971  hoadd32i  32071  cnvadj  32185  hh0oi  32196  hhcno  32197  hhcnf  32198  nmopnegi  32258  lnophmlem2  32310  branmfn  32398  dmrab  32784  3unrab  32790  abrexexd  32796  cbviunf  32841  maprnin  33017  dpmul10  33155  dpexpp1  33168  dpadd3  33172  dpmul  33173  dpmul4  33174  psgnfzto1st  33366  cycpmconjs  33417  fracbas  33569  cos9thpiminplylem5  34121  lmlimxrge0  34283  zrhre  34354  qqhre  34355  rrhre  34356  cbvesum  34377  cbvesumv  34378  unibrsiga  34521  eulerpartlemt  34706  eulerpartgbij  34707  ballotlemrinv  34869  hgt750lem2  34984  bnj1146  35124  bnj893  35261  bnj1234  35346  r11  35430  r12  35431  subfacp1lem1  35570  kur14lem2  35598  kur14lem5  35601  kur14lem7  35603  cvmscld  35664  satfv1lem  35753  fmla0  35773  mvtval  35891  mthmpps  35973  fixun  36298  rabeqbii  36595  iuneq12i  36596  iineq1i  36597  iineq12i  36598  riotaeqbii  36599  ixpeq1i  36601  sumeq2si  36603  prodeq2si  36605  itgeq12i  36607  ditgeq123i  36610  cbvcsbvw2  36632  cbviunvw2  36633  cbviinvw2  36634  cbvmptvw2  36635  cbvriotavw2  36637  cbvoprab1vw  36638  cbvoprab2vw  36639  cbvoprab123vw  36640  cbvoprab23vw  36641  cbvoprab13vw  36642  cbvmpovw2  36643  cbvmpo1vw2  36644  cbvmpo2vw2  36645  cbvixpvw2  36646  cbvprodvw2  36648  cbvitgvw2  36649  cbvditgvw2  36650  ttcun  36912  ttciun  36914  bj-inrab  37451  bj-inrab3  37453  bj-gabeqis  37462  bj-pr1un  37527  bj-pr2un  37541  bj-dfid2ALT  37589  bj-mpomptALT  37649  rnmptsn  37869  f1omptsnlem  37870  rabiun  38132  phpreu  38143  poimirlem18  38177  ovoliunnfl  38201  voliunnfl  38203  mbfposadd  38206  asindmre  38242  abeqin  38793  rncnvepres  38848  qsresid  38870  dmxrn  38926  rnxrn  38960  xrnres  38964  xrnres2  38965  xrnres3  38966  dmxrncnvepres2  38972  dfsucmap3  39002  dfsucmap2  39003  rncossdmcoss  39084  1cosscnvxrn  39104  refrelsredund4  39255  mpets  39495  dfpetparts2  39511  dfpeters2  39513  petseq  39515  pets2eq  39516  cdleme25cv  41022  sn-iotalemcor  42883  sqdeccom12  42940  sumcubes  42964  resuppsinopn  43014  sn-00idlem2  43050  sn-1ticom  43086  mendsca  43804  areaquad  43835  onsucrn  43890  df3o2  43932  df3o3  43933  omcl3g  43953  dfno2  44046  cnvrcl0  44243  sqrtcvallem1  44249  trclrelexplem  44329  iuneq1i  45696  cbvmpo2  45707  cbvmpo1  45708  cbvrabv2w  45738  mptssid  45848  fprodabs2  46203  stoweidlem13  46619  wallispilem4  46674  fourierdlem94  46806  fourierdlem102  46814  fourierdlem111  46823  fourierdlem112  46824  fourierdlem113  46825  fourierdlem114  46826  41prothprmlem2  48259  2exp340mod341  48387  8exp8mod9  48390  nfermltl8rev  48396  stgr1  48615  gpgprismgr4cycllem6  48754  gpgprismgr4cycllem9  48757  gpgprismgr4cycllem10  48758  cbvmpox2  49001  dmmpossx2  49002  zlmodzxzequa  49161  zlmodzxzequap  49164  resinsn  49535  dfswapf2  49924