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  3407  cbvrabv  3413  rabrab  3427  cbvrabw  3438  cbvrabwOLD  3439  cbvrab  3443  cbvcsbw  3869  cbvcsb  3870  cbvcsbv  3871  csbcow  3874  csbco  3875  cbvrabcsfw  3900  cbvrabcsf  3904  un4  4134  incom  4168  in13  4190  in31  4191  in4  4193  symdifcom  4213  indifcom  4242  indir  4245  undir  4246  indifdir  4254  difdif2  4255  notrab  4281  dfnul3  4296  dfif5  4501  rabsnifsb  4682  prcom  4692  tprot  4709  tpcoma  4710  tpcomb  4711  tpass  4712  qdassr  4714  pw0  4772  pwpw0  4773  pwsn  4860  cbviun  4995  cbviin  4996  cbviung  4997  cbviing  4998  cbviunv  4999  cbviinv  5000  iunrab  5011  iunin1  5031  iinuni  5057  cbvopab  5174  cbvopabv  5175  cbvopab1  5176  cbvopab1g  5177  cbvopab2  5178  cbvopab1s  5179  cbvopab1v  5180  cbvopab2v  5181  unopab  5182  cbvmptf  5202  cbvmptfg  5203  cbvmptv  5206  iunopab  5514  dfid4  5527  dfid2  5528  dfid3  5529  rabxp  5679  fconstmpt  5693  csbxp  5730  inxpOLD  5786  cnvco  5839  csbdm  5851  rnmpt  5910  csbres  5942  resundi  5953  resundir  5954  resindi  5955  resindir  5956  rescom  5962  resima  5975  imadmrn  6030  cnvimarndm  6043  cnvi  6102  cnvin  6105  rnun  6106  imaundi  6110  cnvxp  6118  imainrect  6142  csbrn  6164  imacnvcnv  6167  resdmres  6193  imadmres  6195  resdifdir  6198  mptpreima  6199  dfpred3  6273  predin  6288  predun  6289  preddif  6290  frpoind  6303  cbviotaw  6459  cbviotavw  6460  cbviota  6461  sb8iota  6463  resdif  6803  opabiotadm  6924  fndmin  6999  fninfp  7130  cbvriotaw  7335  cbvriotavw  7336  cbvriota  7339  riotarab  7368  dfoprab2  7427  cbvoprab1  7456  cbvoprab2  7457  cbvoprab12  7458  cbvoprab12v  7459  cbvoprab3  7460  cbvoprab3v  7461  cbvmpox  7462  cbvmpov  7464  resoprab  7487  caov32  7596  caov31  7598  caov4  7600  caovlem2  7605  uniuni  7718  zfrep6  7913  ofmres  7942  dfopab2  8010  dfxp3  8019  dmmpossx  8024  fmpox  8025  fsplit  8073  ovtpos  8197  tposco  8213  frrlem5  8246  tfrlem10  8332  o2p2e4  8482  0map0sn0  8835  mapsncnv  8843  cbvixp  8864  cbvixpv  8865  xpcomco  9008  sbthlem6  9033  1sdomOLD  9172  ttrclresv  9646  frind  9679  cardf2  9872  alephcard  9999  alephfplem1  10033  xp2dju  10106  djuassen  10108  infdju1  10119  pwdju1  10120  ackbij1lem14  10161  compsscnv  10300  dffin1-5  10317  ituniiun  10351  axdc2lem  10377  axdc3lem4  10382  axcclem  10386  pwcfsdom  10512  dmaddpi  10819  dmmulpi  10820  adderpqlem  10883  addassnq  10887  mulcanenq  10889  addcmpblnr  10998  mulcmpblnrlem  10999  ltsrpr  11006  mulgt0sr  11034  sqgt0sr  11035  axi2m1  11088  negiso  12139  nummac  12670  decsubi  12688  9t11e99  12755  fztpval  13523  seqval  13953  sqrecii  14124  sqdivi  14126  binom2i  14153  4bc2eq6  14270  hashgval  14274  revs1  14706  cats1cat  14803  trclublem  14937  shftdm  15013  shftidt2  15023  cji  15101  cbvsum  15637  cbvsumv  15638  sumfc  15651  ackbijnn  15770  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  prodfc  15887  fsumcube  16002  divalglem2  16341  nn0expgcd  16510  nn0gcdsq  16698  prmreclem2  16864  prmrec  16869  hashbc0  16952  dec5nprm  17013  dec2nprm  17014  gcdi  17020  decsplit  17029  1259lem1  17077  1259lem4  17080  4001lem1  17087  phlstr  17285  oduval  18229  oduleval  18230  odubas  18232  lubdm  18290  glbdm  18303  oppgid  19270  symgbas0  19303  gsumcom2  19889  ringidval  20103  oppr1  20270  dfrhm2  20394  rmodislmod  20868  cnfldsub  21339  cnflddiv  21342  cnflddivOLD  21343  dvdsrzring  21403  pjdm  21649  pjfval2  21651  opsrtoslem1  21995  restco  23084  ufprim  23829  tgioo3  24727  oprpiece1res1  24882  oprpiece1res2  24883  volfiniun  25481  vitalilem4  25545  cbvitg  25710  cbvitgv  25711  itgresr  25713  cbvditg  25788  plyid  26147  coeidp  26202  dgrid  26203  sincos3rdpi  26459  logblog  26735  ang180lem2  26753  1cubrlem  26784  asin1  26837  log2ublem2  26890  log2ublem3  26891  emcllem5  26943  lgsdir2lem5  27273  lgsquadlem3  27326  2lgslem1b  27336  2lgsoddprmlem3d  27357  noextend  27611  nosupbday  27650  nosupbnd1  27659  nosupbnd2  27661  noinfbday  27665  noinfbnd1  27674  dmscut  27757  madeval2  27798  negs0s  27972  negs1s  27973  1p1e2s  28343  cchhllem  28867  ax5seglem7  28915  vtxval0  29019  iedgval0  29020  finsumvtxdg2ssteplem1  29526  wwlksnfi  29886  1wlkdlem1  30116  ex-un  30403  ex-pw  30408  ex-cnv  30416  ex-co  30417  bafval  30583  vsfval  30612  cnnvba  30658  cnnvm  30661  ip2dii  30823  siilem1  30830  h2hcau  30958  hvsubsub4i  31038  hvnegdii  31041  normlem3  31091  normlem8  31096  norm-iii-i  31118  normpar2i  31135  polid2i  31136  chjassi  31465  chj4i  31502  h1de2i  31532  spanunsni  31558  fh3i  31602  fh4i  31603  qlax4i  31609  qlaxr3i  31615  3oalem5  31645  pjadjii  31653  pjsubii  31657  hoadd32i  31757  cnvadj  31871  hh0oi  31882  hhcno  31883  hhcnf  31884  nmopnegi  31944  lnophmlem2  31996  branmfn  32084  dmrab  32476  3unrab  32482  abrexexd  32488  cbviunf  32534  maprnin  32704  dpmul10  32865  dpexpp1  32878  dpadd3  32882  dpmul  32883  dpmul4  32884  psgnfzto1st  33077  cycpmconjs  33128  fracbas  33271  cos9thpiminplylem5  33769  lmlimxrge0  33931  zrhre  34002  qqhre  34003  rrhre  34004  cbvesum  34025  cbvesumv  34026  unibrsiga  34169  eulerpartlemt  34355  eulerpartgbij  34356  ballotlemrinv  34518  hgt750lem2  34636  bnj1146  34774  bnj893  34911  bnj1234  34996  subfacp1lem1  35159  kur14lem2  35187  kur14lem5  35190  kur14lem7  35192  cvmscld  35253  satfv1lem  35342  fmla0  35362  mvtval  35480  mthmpps  35562  fixun  35890  rabeqbii  36175  iuneq12i  36176  iineq1i  36177  iineq12i  36178  riotaeqbii  36179  ixpeq1i  36181  sumeq2si  36183  prodeq2si  36185  itgeq12i  36187  ditgeq123i  36190  cbvcsbvw2  36212  cbviunvw2  36213  cbviinvw2  36214  cbvmptvw2  36215  cbvriotavw2  36217  cbvoprab1vw  36218  cbvoprab2vw  36219  cbvoprab123vw  36220  cbvoprab23vw  36221  cbvoprab13vw  36222  cbvmpovw2  36223  cbvmpo1vw2  36224  cbvmpo2vw2  36225  cbvixpvw2  36226  cbvprodvw2  36228  cbvitgvw2  36229  cbvditgvw2  36230  bj-inrab  36908  bj-inrab3  36910  bj-gabeqis  36919  bj-pr1un  36984  bj-pr2un  36998  bj-dfid2ALT  37046  bj-mpomptALT  37100  rnmptsn  37316  f1omptsnlem  37317  rabiun  37580  phpreu  37591  poimirlem18  37625  ovoliunnfl  37649  voliunnfl  37651  mbfposadd  37654  asindmre  37690  abeqin  38234  rncnvepres  38284  qsresid  38306  dmxrn  38353  rnxrn  38377  xrnres  38381  xrnres2  38382  xrnres3  38383  rncossdmcoss  38439  1cosscnvxrn  38459  refrelsredund4  38616  mpets  38827  cdleme25cv  40345  sn-iotalemcor  42203  sqdeccom12  42270  sumcubes  42294  resuppsinopn  42344  sn-00idlem2  42380  sn-1ticom  42416  mendsca  43167  areaquad  43198  onsucrn  43253  df3o2  43295  df3o3  43296  omcl3g  43316  dfno2  43410  cnvrcl0  43607  sqrtcvallem1  43613  trclrelexplem  43693  iuneq1i  45072  cbvmpo2  45084  cbvmpo1  45085  cbvrabv2w  45115  mptssid  45228  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  47953  gpgprismgr4cycllem6  48083  gpgprismgr4cycllem9  48086  gpgprismgr4cycllem10  48087  cbvmpox2  48317  dmmpossx2  48318  zlmodzxzequa  48478  zlmodzxzequap  48481  resinsn  48853  dfswapf2  49243