Theorem 3eqtr4i 2762

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  rabbiiaOLD  3399  cbvrabv  3405  rabrab  3419  cbvrabw  3430  cbvrabwOLD  3431  cbvrab  3435  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbcow  3866  csbco  3867  cbvrabcsfw  3892  cbvrabcsf  3896  un4  4126  incom  4160  in13  4182  in31  4183  in4  4185  symdifcom  4205  indifcom  4234  indir  4237  undir  4238  indifdir  4246  difdif2  4247  notrab  4273  dfnul3  4288  dfif5  4493  rabsnifsb  4674  prcom  4684  tprot  4701  tpcoma  4702  tpcomb  4703  tpass  4704  qdassr  4706  pw0  4763  pwpw0  4764  pwsn  4851  cbviun  4985  cbviin  4986  cbviung  4987  cbviing  4988  cbviunv  4989  cbviinv  4990  iunrab  5001  iunin1  5021  iinuni  5047  cbvopab  5164  cbvopabv  5165  cbvopab1  5166  cbvopab1g  5167  cbvopab2  5168  cbvopab1s  5169  cbvopab1v  5170  cbvopab2v  5171  unopab  5172  cbvmptf  5192  cbvmptfg  5193  cbvmptv  5196  iunopab  5502  dfid4  5515  dfid2  5516  dfid3  5517  rabxp  5667  fconstmpt  5681  csbxp  5719  inxpOLD  5775  cnvco  5828  csbdm  5840  rnmpt  5899  csbres  5933  resundi  5944  resundir  5945  resindi  5946  resindir  5947  rescom  5953  resima  5966  imadmrn  6021  cnvimarndm  6034  cnvi  6090  cnvin  6093  rnun  6094  imaundi  6098  cnvxp  6106  imainrect  6130  csbrn  6152  imacnvcnv  6155  resdmres  6181  imadmres  6183  resdifdir  6186  mptpreima  6187  dfpred3  6260  predin  6275  predun  6276  preddif  6277  frpoind  6290  cbviotaw  6445  cbviotavw  6446  cbviota  6447  sb8iota  6449  resdif  6785  opabiotadm  6904  fndmin  6979  fninfp  7110  cbvriotaw  7315  cbvriotavw  7316  cbvriota  7319  riotarab  7348  dfoprab2  7407  cbvoprab1  7436  cbvoprab2  7437  cbvoprab12  7438  cbvoprab12v  7439  cbvoprab3  7440  cbvoprab3v  7441  cbvmpox  7442  cbvmpov  7444  resoprab  7467  caov32  7576  caov31  7578  caov4  7580  caovlem2  7585  uniuni  7698  zfrep6  7890  ofmres  7919  dfopab2  7987  dfxp3  7996  dmmpossx  8001  fmpox  8002  fsplit  8050  ovtpos  8174  tposco  8190  frrlem5  8223  tfrlem10  8309  o2p2e4  8459  0map0sn0  8812  mapsncnv  8820  cbvixp  8841  cbvixpv  8842  xpcomco  8984  sbthlem6  9009  ttrclresv  9613  frind  9646  cardf2  9839  alephcard  9964  alephfplem1  9998  xp2dju  10071  djuassen  10073  infdju1  10084  pwdju1  10085  ackbij1lem14  10126  compsscnv  10265  dffin1-5  10282  ituniiun  10316  axdc2lem  10342  axdc3lem4  10347  axcclem  10351  pwcfsdom  10477  dmaddpi  10784  dmmulpi  10785  adderpqlem  10848  addassnq  10852  mulcanenq  10854  addcmpblnr  10963  mulcmpblnrlem  10964  ltsrpr  10971  mulgt0sr  10999  sqgt0sr  11000  axi2m1  11053  negiso  12105  nummac  12636  decsubi  12654  9t11e99  12721  fztpval  13489  seqval  13919  sqrecii  14090  sqdivi  14092  binom2i  14119  4bc2eq6  14236  hashgval  14240  revs1  14671  cats1cat  14768  trclublem  14902  shftdm  14978  shftidt2  14988  cji  15066  cbvsum  15602  cbvsumv  15603  sumfc  15616  ackbijnn  15735  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  prodfc  15852  fsumcube  15967  divalglem2  16306  nn0expgcd  16475  nn0gcdsq  16663  prmreclem2  16829  prmrec  16834  hashbc0  16917  dec5nprm  16978  dec2nprm  16979  gcdi  16985  decsplit  16994  1259lem1  17042  1259lem4  17045  4001lem1  17052  phlstr  17250  oduval  18194  oduleval  18195  odubas  18197  lubdm  18255  glbdm  18268  oppgid  19235  symgbas0  19268  gsumcom2  19854  ringidval  20068  oppr1  20235  dfrhm2  20359  rmodislmod  20833  cnfldsub  21304  cnflddiv  21307  cnflddivOLD  21308  dvdsrzring  21368  pjdm  21614  pjfval2  21616  opsrtoslem1  21960  restco  23049  ufprim  23794  tgioo3  24692  oprpiece1res1  24847  oprpiece1res2  24848  volfiniun  25446  vitalilem4  25510  cbvitg  25675  cbvitgv  25676  itgresr  25678  cbvditg  25753  plyid  26112  coeidp  26167  dgrid  26168  sincos3rdpi  26424  logblog  26700  ang180lem2  26718  1cubrlem  26749  asin1  26802  log2ublem2  26855  log2ublem3  26856  emcllem5  26908  lgsdir2lem5  27238  lgsquadlem3  27291  2lgslem1b  27301  2lgsoddprmlem3d  27322  noextend  27576  nosupbday  27615  nosupbnd1  27624  nosupbnd2  27626  noinfbday  27630  noinfbnd1  27639  dmscut  27722  madeval2  27763  negs0s  27937  negs1s  27938  1p1e2s  28308  cchhllem  28832  ax5seglem7  28880  vtxval0  28984  iedgval0  28985  finsumvtxdg2ssteplem1  29491  wwlksnfi  29851  1wlkdlem1  30081  ex-un  30368  ex-pw  30373  ex-cnv  30381  ex-co  30382  bafval  30548  vsfval  30577  cnnvba  30623  cnnvm  30626  ip2dii  30788  siilem1  30795  h2hcau  30923  hvsubsub4i  31003  hvnegdii  31006  normlem3  31056  normlem8  31061  norm-iii-i  31083  normpar2i  31100  polid2i  31101  chjassi  31430  chj4i  31467  h1de2i  31497  spanunsni  31523  fh3i  31567  fh4i  31568  qlax4i  31574  qlaxr3i  31580  3oalem5  31610  pjadjii  31618  pjsubii  31622  hoadd32i  31722  cnvadj  31836  hh0oi  31847  hhcno  31848  hhcnf  31849  nmopnegi  31909  lnophmlem2  31961  branmfn  32049  dmrab  32441  3unrab  32447  abrexexd  32453  cbviunf  32499  maprnin  32675  dpmul10  32836  dpexpp1  32849  dpadd3  32853  dpmul  32854  dpmul4  32855  psgnfzto1st  33048  cycpmconjs  33099  fracbas  33245  cos9thpiminplylem5  33759  lmlimxrge0  33921  zrhre  33992  qqhre  33993  rrhre  33994  cbvesum  34015  cbvesumv  34016  unibrsiga  34159  eulerpartlemt  34345  eulerpartgbij  34346  ballotlemrinv  34508  hgt750lem2  34626  bnj1146  34764  bnj893  34901  bnj1234  34986  subfacp1lem1  35162  kur14lem2  35190  kur14lem5  35193  kur14lem7  35195  cvmscld  35256  satfv1lem  35345  fmla0  35365  mvtval  35483  mthmpps  35565  fixun  35893  rabeqbii  36178  iuneq12i  36179  iineq1i  36180  iineq12i  36181  riotaeqbii  36182  ixpeq1i  36184  sumeq2si  36186  prodeq2si  36188  itgeq12i  36190  ditgeq123i  36193  cbvcsbvw2  36215  cbviunvw2  36216  cbviinvw2  36217  cbvmptvw2  36218  cbvriotavw2  36220  cbvoprab1vw  36221  cbvoprab2vw  36222  cbvoprab123vw  36223  cbvoprab23vw  36224  cbvoprab13vw  36225  cbvmpovw2  36226  cbvmpo1vw2  36227  cbvmpo2vw2  36228  cbvixpvw2  36229  cbvprodvw2  36231  cbvitgvw2  36232  cbvditgvw2  36233  bj-inrab  36911  bj-inrab3  36913  bj-gabeqis  36922  bj-pr1un  36987  bj-pr2un  37001  bj-dfid2ALT  37049  bj-mpomptALT  37103  rnmptsn  37319  f1omptsnlem  37320  rabiun  37583  phpreu  37594  poimirlem18  37628  ovoliunnfl  37652  voliunnfl  37654  mbfposadd  37657  asindmre  37693  abeqin  38237  rncnvepres  38287  qsresid  38309  dmxrn  38356  rnxrn  38380  xrnres  38384  xrnres2  38385  xrnres3  38386  rncossdmcoss  38442  1cosscnvxrn  38462  refrelsredund4  38619  mpets  38830  cdleme25cv  40347  sn-iotalemcor  42205  sqdeccom12  42272  sumcubes  42296  resuppsinopn  42346  sn-00idlem2  42382  sn-1ticom  42418  mendsca  43168  areaquad  43199  onsucrn  43254  df3o2  43296  df3o3  43297  omcl3g  43317  dfno2  43411  cnvrcl0  43608  sqrtcvallem1  43614  trclrelexplem  43694  iuneq1i  45073  cbvmpo2  45085  cbvmpo1  45086  cbvrabv2w  45116  mptssid  45229  fprodabs2  45586  stoweidlem13  46004  wallispilem4  46059  fourierdlem94  46191  fourierdlem102  46199  fourierdlem111  46208  fourierdlem112  46209  fourierdlem113  46210  fourierdlem114  46211  41prothprmlem2  47612  2exp340mod341  47727  8exp8mod9  47730  nfermltl8rev  47736  stgr1  47955  gpgprismgr4cycllem6  48094  gpgprismgr4cycllem9  48097  gpgprismgr4cycllem10  48098  cbvmpox2  48330  dmmpossx2  48331  zlmodzxzequa  48491  zlmodzxzequap  48494  resinsn  48866  dfswapf2  49256