Theorem 3eqtr4i 2763

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

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

This theorem is referenced by:  rabbiiaOLD  3413  cbvrabv  3419  rabrab  3433  cbvrabw  3444  cbvrabwOLD  3445  cbvrab  3449  cbvcsbw  3875  cbvcsb  3876  cbvcsbv  3877  csbcow  3880  csbco  3881  cbvrabcsfw  3906  cbvrabcsf  3910  un4  4141  incom  4175  in13  4197  in31  4198  in4  4200  symdifcom  4220  indifcom  4249  indir  4252  undir  4253  indifdir  4261  difdif2  4262  notrab  4288  dfnul3  4303  dfif5  4508  rabsnifsb  4689  prcom  4699  tprot  4716  tpcoma  4717  tpcomb  4718  tpass  4719  qdassr  4721  pw0  4779  pwpw0  4780  pwsn  4867  cbviun  5003  cbviin  5004  cbviung  5005  cbviing  5006  cbviunv  5007  cbviinv  5008  iunrab  5019  iunin1  5039  iinuni  5065  cbvopab  5182  cbvopabv  5183  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  cbvopab1v  5188  cbvopab2v  5189  unopab  5190  cbvmptf  5210  cbvmptfg  5211  cbvmptv  5214  iunopab  5522  iunopabOLD  5523  dfid4  5537  dfid2  5538  dfid3  5539  rabxp  5689  fconstmpt  5703  csbxp  5741  inxpOLD  5799  cnvco  5852  csbdm  5864  rnmpt  5924  csbres  5956  resundi  5967  resundir  5968  resindi  5969  resindir  5970  rescom  5976  resima  5989  imadmrn  6044  cnvimarndm  6057  cnvi  6117  cnvin  6120  rnun  6121  imaundi  6125  cnvxp  6133  imainrect  6157  csbrn  6179  imacnvcnv  6182  resdmres  6208  imadmres  6210  resdifdir  6213  mptpreima  6214  dfpred3  6288  predin  6303  predun  6304  preddif  6305  frpoind  6318  cbviotaw  6474  cbviotavw  6475  cbviota  6476  sb8iota  6478  resdif  6824  opabiotadm  6945  fndmin  7020  fninfp  7151  cbvriotaw  7356  cbvriotavw  7357  cbvriota  7360  riotarab  7389  dfoprab2  7450  cbvoprab1  7479  cbvoprab2  7480  cbvoprab12  7481  cbvoprab12v  7482  cbvoprab3  7483  cbvoprab3v  7484  cbvmpox  7485  cbvmpov  7487  resoprab  7510  caov32  7619  caov31  7621  caov4  7623  caovlem2  7628  uniuni  7741  zfrep6  7936  ofmres  7966  dfopab2  8034  dfxp3  8043  dmmpossx  8048  fmpox  8049  fsplit  8099  ovtpos  8223  tposco  8239  frrlem5  8272  tfrlem10  8358  o2p2e4  8508  0map0sn0  8861  mapsncnv  8869  cbvixp  8890  cbvixpv  8891  xpcomco  9036  sbthlem6  9062  1sdomOLD  9203  ttrclresv  9677  frind  9710  cardf2  9903  alephcard  10030  alephfplem1  10064  xp2dju  10137  djuassen  10139  infdju1  10150  pwdju1  10151  ackbij1lem14  10192  compsscnv  10331  dffin1-5  10348  ituniiun  10382  axdc2lem  10408  axdc3lem4  10413  axcclem  10417  pwcfsdom  10543  dmaddpi  10850  dmmulpi  10851  adderpqlem  10914  addassnq  10918  mulcanenq  10920  addcmpblnr  11029  mulcmpblnrlem  11030  ltsrpr  11037  mulgt0sr  11065  sqgt0sr  11066  axi2m1  11119  negiso  12170  nummac  12701  decsubi  12719  9t11e99  12786  fztpval  13554  seqval  13984  sqrecii  14155  sqdivi  14157  binom2i  14184  4bc2eq6  14301  hashgval  14305  revs1  14737  cats1cat  14834  trclublem  14968  shftdm  15044  shftidt2  15054  cji  15132  cbvsum  15668  cbvsumv  15669  sumfc  15682  ackbijnn  15801  cbvprod  15886  cbvprodv  15887  prodeq1i  15889  prodfc  15918  fsumcube  16033  divalglem2  16372  nn0expgcd  16541  nn0gcdsq  16729  prmreclem2  16895  prmrec  16900  hashbc0  16983  dec5nprm  17044  dec2nprm  17045  gcdi  17051  decsplit  17060  1259lem1  17108  1259lem4  17111  4001lem1  17118  phlstr  17316  oduval  18256  oduleval  18257  odubas  18259  lubdm  18317  glbdm  18330  oppgid  19295  symgbas0  19326  gsumcom2  19912  ringidval  20099  oppr1  20266  dfrhm2  20390  rmodislmod  20843  cnfldsub  21316  cnflddiv  21319  cnflddivOLD  21320  dvdsrzring  21378  pjdm  21623  pjfval2  21625  opsrtoslem1  21969  restco  23058  ufprim  23803  tgioo3  24701  oprpiece1res1  24856  oprpiece1res2  24857  volfiniun  25455  vitalilem4  25519  cbvitg  25684  cbvitgv  25685  itgresr  25687  cbvditg  25762  plyid  26121  coeidp  26176  dgrid  26177  sincos3rdpi  26433  logblog  26709  ang180lem2  26727  1cubrlem  26758  asin1  26811  log2ublem2  26864  log2ublem3  26865  emcllem5  26917  lgsdir2lem5  27247  lgsquadlem3  27300  2lgslem1b  27310  2lgsoddprmlem3d  27331  noextend  27585  nosupbday  27624  nosupbnd1  27633  nosupbnd2  27635  noinfbday  27639  noinfbnd1  27648  dmscut  27730  madeval2  27768  negs0s  27939  negs1s  27940  1p1e2s  28309  cchhllem  28821  ax5seglem7  28869  vtxval0  28973  iedgval0  28974  finsumvtxdg2ssteplem1  29480  wwlksnfi  29843  1wlkdlem1  30073  ex-un  30360  ex-pw  30365  ex-cnv  30373  ex-co  30374  bafval  30540  vsfval  30569  cnnvba  30615  cnnvm  30618  ip2dii  30780  siilem1  30787  h2hcau  30915  hvsubsub4i  30995  hvnegdii  30998  normlem3  31048  normlem8  31053  norm-iii-i  31075  normpar2i  31092  polid2i  31093  chjassi  31422  chj4i  31459  h1de2i  31489  spanunsni  31515  fh3i  31559  fh4i  31560  qlax4i  31566  qlaxr3i  31572  3oalem5  31602  pjadjii  31610  pjsubii  31614  hoadd32i  31714  cnvadj  31828  hh0oi  31839  hhcno  31840  hhcnf  31841  nmopnegi  31901  lnophmlem2  31953  branmfn  32041  dmrab  32433  3unrab  32439  abrexexd  32445  cbviunf  32491  maprnin  32661  dpmul10  32822  dpexpp1  32835  dpadd3  32839  dpmul  32840  dpmul4  32841  psgnfzto1st  33069  cycpmconjs  33120  fracbas  33262  cos9thpiminplylem5  33783  lmlimxrge0  33945  zrhre  34016  qqhre  34017  rrhre  34018  cbvesum  34039  cbvesumv  34040  unibrsiga  34183  eulerpartlemt  34369  eulerpartgbij  34370  ballotlemrinv  34532  hgt750lem2  34650  bnj1146  34788  bnj893  34925  bnj1234  35010  subfacp1lem1  35173  kur14lem2  35201  kur14lem5  35204  kur14lem7  35206  cvmscld  35267  satfv1lem  35356  fmla0  35376  mvtval  35494  mthmpps  35576  fixun  35904  rabeqbii  36189  iuneq12i  36190  iineq1i  36191  iineq12i  36192  riotaeqbii  36193  ixpeq1i  36195  sumeq2si  36197  prodeq2si  36199  itgeq12i  36201  ditgeq123i  36204  cbvcsbvw2  36226  cbviunvw2  36227  cbviinvw2  36228  cbvmptvw2  36229  cbvriotavw2  36231  cbvoprab1vw  36232  cbvoprab2vw  36233  cbvoprab123vw  36234  cbvoprab23vw  36235  cbvoprab13vw  36236  cbvmpovw2  36237  cbvmpo1vw2  36238  cbvmpo2vw2  36239  cbvixpvw2  36240  cbvprodvw2  36242  cbvitgvw2  36243  cbvditgvw2  36244  bj-inrab  36922  bj-inrab3  36924  bj-gabeqis  36933  bj-pr1un  36998  bj-pr2un  37012  bj-dfid2ALT  37060  bj-mpomptALT  37114  rnmptsn  37330  f1omptsnlem  37331  rabiun  37594  phpreu  37605  poimirlem18  37639  ovoliunnfl  37663  voliunnfl  37665  mbfposadd  37668  asindmre  37704  abeqin  38248  rncnvepres  38298  qsresid  38320  dmxrn  38367  rnxrn  38391  xrnres  38395  xrnres2  38396  xrnres3  38397  rncossdmcoss  38453  1cosscnvxrn  38473  refrelsredund4  38630  mpets  38841  cdleme25cv  40359  sn-iotalemcor  42217  sqdeccom12  42284  sumcubes  42308  resuppsinopn  42358  sn-00idlem2  42394  sn-1ticom  42430  mendsca  43181  areaquad  43212  onsucrn  43267  df3o2  43309  df3o3  43310  omcl3g  43330  dfno2  43424  cnvrcl0  43621  sqrtcvallem1  43627  trclrelexplem  43707  iuneq1i  45086  cbvmpo2  45098  cbvmpo1  45099  cbvrabv2w  45129  mptssid  45242  fprodabs2  45600  stoweidlem13  46018  wallispilem4  46073  fourierdlem94  46205  fourierdlem102  46213  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fourierdlem114  46225  41prothprmlem2  47623  2exp340mod341  47738  8exp8mod9  47741  nfermltl8rev  47747  stgr1  47964  gpgprismgr4cycllem6  48094  gpgprismgr4cycllem9  48097  gpgprismgr4cycllem10  48098  cbvmpox2  48328  dmmpossx2  48329  zlmodzxzequa  48489  zlmodzxzequap  48492  resinsn  48864  dfswapf2  49254