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  35604  kur14lem2  35632  kur14lem5  35635  kur14lem7  35637  cvmscld  35698  satfv1lem  35787  fmla0  35807  mvtval  35925  mthmpps  36007  fixun  36332  rabeqbii  36629  iuneq12i  36630  iineq1i  36631  iineq12i  36632  riotaeqbii  36633  ixpeq1i  36635  sumeq2si  36637  prodeq2si  36639  itgeq12i  36641  ditgeq123i  36644  cbvcsbvw2  36666  cbviunvw2  36667  cbviinvw2  36668  cbvmptvw2  36669  cbvriotavw2  36671  cbvoprab1vw  36672  cbvoprab2vw  36673  cbvoprab123vw  36674  cbvoprab23vw  36675  cbvoprab13vw  36676  cbvmpovw2  36677  cbvmpo1vw2  36678  cbvmpo2vw2  36679  cbvixpvw2  36680  cbvprodvw2  36682  cbvitgvw2  36683  cbvditgvw2  36684  ttcun  36946  ttciun  36948  bj-inrab  37485  bj-inrab3  37487  bj-gabeqis  37496  bj-pr1un  37561  bj-pr2un  37575  bj-dfid2ALT  37623  bj-mpomptALT  37683  rnmptsn  37903  f1omptsnlem  37904  rabiun  38166  phpreu  38177  poimirlem18  38211  ovoliunnfl  38235  voliunnfl  38237  mbfposadd  38240  asindmre  38276  abeqin  38827  rncnvepres  38882  qsresid  38904  dmxrn  38960  rnxrn  38994  xrnres  38998  xrnres2  38999  xrnres3  39000  dmxrncnvepres2  39006  dfsucmap3  39036  dfsucmap2  39037  rncossdmcoss  39118  1cosscnvxrn  39138  refrelsredund4  39289  mpets  39529  dfpetparts2  39545  dfpeters2  39547  petseq  39549  pets2eq  39550  cdleme25cv  41056  sn-iotalemcor  42917  sqdeccom12  42974  sumcubes  42998  resuppsinopn  43048  sn-00idlem2  43084  sn-1ticom  43120  mendsca  43838  areaquad  43869  onsucrn  43924  df3o2  43966  df3o3  43967  omcl3g  43987  dfno2  44080  cnvrcl0  44277  sqrtcvallem1  44283  trclrelexplem  44363  iuneq1i  45730  cbvmpo2  45741  cbvmpo1  45742  cbvrabv2w  45772  mptssid  45882  fprodabs2  46237  stoweidlem13  46653  wallispilem4  46708  fourierdlem94  46840  fourierdlem102  46848  fourierdlem111  46857  fourierdlem112  46858  fourierdlem113  46859  fourierdlem114  46860  41prothprmlem2  48293  2exp340mod341  48421  8exp8mod9  48424  nfermltl8rev  48430  stgr1  48649  gpgprismgr4cycllem6  48788  gpgprismgr4cycllem9  48791  gpgprismgr4cycllem10  48792  cbvmpox2  49035  dmmpossx2  49036  zlmodzxzequa  49195  zlmodzxzequap  49198  resinsn  49569  dfswapf2  49958