Theorem 3eqtr4i 2770

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  cbvrabv  3411  rabrab  3425  cbvrabw  3436  cbvrabwOLD  3437  cbvrab  3441  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbcow  3866  csbco  3867  cbvrabcsfw  3892  cbvrabcsf  3896  un4  4129  incom  4163  in13  4185  in31  4186  in4  4188  symdifcom  4208  indifcom  4237  indir  4240  undir  4241  indifdir  4249  difdif2  4250  notrab  4276  dfnul3  4291  dfif5  4498  rabsnifsb  4681  prcom  4691  tprot  4708  tpcoma  4709  tpcomb  4710  tpass  4711  qdassr  4713  pw0  4770  pwpw0  4771  pwsn  4858  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iunrab  5010  iunin1  5029  iinuni  5055  cbvopab  5172  cbvopabv  5173  cbvopab1  5174  cbvopab1g  5175  cbvopab2  5176  cbvopab1s  5177  cbvopab1v  5178  cbvopab2v  5179  unopab  5180  cbvmptf  5200  cbvmptfg  5201  cbvmptv  5204  iunopab  5515  dfid4  5528  dfid2  5529  dfid3  5530  rabxp  5680  fconstmpt  5694  csbxp  5733  inxpOLD  5789  cnvco  5842  csbdm  5854  rnmpt  5914  csbres  5949  resundi  5960  resundir  5961  resindi  5962  resindir  5963  rescom  5969  resima  5982  imadmrn  6037  cnvimarndm  6050  cnvi  6107  cnvin  6110  rnun  6111  imaundi  6115  cnvxp  6123  imainrect  6147  csbrn  6169  imacnvcnv  6172  resdmres  6198  imadmres  6200  resdifdir  6203  mptpreima  6204  dfpred3  6278  predin  6293  predun  6294  preddif  6295  frpoind  6308  cbviotaw  6463  cbviotavw  6464  cbviota  6465  sb8iota  6467  resdif  6803  opabiotadm  6923  fndmin  6999  fninfp  7130  cbvriotaw  7334  cbvriotavw  7335  cbvriota  7338  riotarab  7367  dfoprab2  7426  cbvoprab1  7455  cbvoprab2  7456  cbvoprab12  7457  cbvoprab12v  7458  cbvoprab3  7459  cbvoprab3v  7460  cbvmpox  7461  cbvmpov  7463  resoprab  7486  caov32  7595  caov31  7597  caov4  7599  caovlem2  7604  uniuni  7717  zfrep6  7909  ofmres  7938  dfopab2  8006  dfxp3  8015  dmmpossx  8020  fmpox  8021  fsplit  8069  ovtpos  8193  tposco  8209  frrlem5  8242  tfrlem10  8328  o2p2e4  8478  0map0sn0  8835  mapsncnv  8843  cbvixp  8864  cbvixpv  8865  xpcomco  9007  sbthlem6  9032  ttrclresv  9638  frind  9674  cardf2  9867  alephcard  9992  alephfplem1  10026  xp2dju  10099  djuassen  10101  infdju1  10112  pwdju1  10113  ackbij1lem14  10154  compsscnv  10293  dffin1-5  10310  ituniiun  10344  axdc2lem  10370  axdc3lem4  10375  axcclem  10379  pwcfsdom  10506  dmaddpi  10813  dmmulpi  10814  adderpqlem  10877  addassnq  10881  mulcanenq  10883  addcmpblnr  10992  mulcmpblnrlem  10993  ltsrpr  11000  mulgt0sr  11028  sqgt0sr  11029  axi2m1  11082  negiso  12134  nummac  12664  decsubi  12682  9t11e99  12749  fztpval  13514  seqval  13947  sqrecii  14118  sqdivi  14120  binom2i  14147  4bc2eq6  14264  hashgval  14268  revs1  14700  cats1cat  14796  trclublem  14930  shftdm  15006  shftidt2  15016  cji  15094  cbvsum  15630  cbvsumv  15631  sumfc  15644  ackbijnn  15763  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  prodfc  15880  fsumcube  15995  divalglem2  16334  nn0expgcd  16503  nn0gcdsq  16691  prmreclem2  16857  prmrec  16862  hashbc0  16945  dec5nprm  17006  dec2nprm  17007  gcdi  17013  decsplit  17022  1259lem1  17070  1259lem4  17073  4001lem1  17080  phlstr  17278  oduval  18223  oduleval  18224  odubas  18226  lubdm  18284  glbdm  18297  oppgid  19300  symgbas0  19333  gsumcom2  19919  ringidval  20133  oppr1  20301  dfrhm2  20425  rmodislmod  20896  cnfldsub  21367  cnflddiv  21370  cnflddivOLD  21371  dvdsrzring  21431  pjdm  21677  pjfval2  21679  opsrtoslem1  22025  restco  23123  ufprim  23868  tgioo3  24765  oprpiece1res1  24920  oprpiece1res2  24921  volfiniun  25519  vitalilem4  25583  cbvitg  25748  cbvitgv  25749  itgresr  25751  cbvditg  25826  plyid  26185  coeidp  26240  dgrid  26241  sincos3rdpi  26497  logblog  26773  ang180lem2  26791  1cubrlem  26822  asin1  26875  log2ublem2  26928  log2ublem3  26929  emcllem5  26981  lgsdir2lem5  27311  lgsquadlem3  27364  2lgslem1b  27374  2lgsoddprmlem3d  27395  noextend  27649  nosupbday  27688  nosupbnd1  27697  nosupbnd2  27699  noinfbday  27703  noinfbnd1  27712  dmcuts  27802  madeval2  27844  neg0s  28037  neg1s  28038  cchhllem  28975  ax5seglem7  29024  vtxval0  29128  iedgval0  29129  finsumvtxdg2ssteplem1  29635  wwlksnfi  29995  1wlkdlem1  30228  ex-un  30515  ex-pw  30520  ex-cnv  30528  ex-co  30529  bafval  30696  vsfval  30725  cnnvba  30771  cnnvm  30774  ip2dii  30936  siilem1  30943  h2hcau  31071  hvsubsub4i  31151  hvnegdii  31154  normlem3  31204  normlem8  31209  norm-iii-i  31231  normpar2i  31248  polid2i  31249  chjassi  31578  chj4i  31615  h1de2i  31645  spanunsni  31671  fh3i  31715  fh4i  31716  qlax4i  31722  qlaxr3i  31728  3oalem5  31758  pjadjii  31766  pjsubii  31770  hoadd32i  31870  cnvadj  31984  hh0oi  31995  hhcno  31996  hhcnf  31997  nmopnegi  32057  lnophmlem2  32109  branmfn  32197  dmrab  32587  3unrab  32594  abrexexd  32600  cbviunf  32646  maprnin  32825  dpmul10  32991  dpexpp1  33004  dpadd3  33008  dpmul  33009  dpmul4  33010  psgnfzto1st  33203  cycpmconjs  33254  fracbas  33403  cos9thpiminplylem5  33968  lmlimxrge0  34130  zrhre  34201  qqhre  34202  rrhre  34203  cbvesum  34224  cbvesumv  34225  unibrsiga  34368  eulerpartlemt  34553  eulerpartgbij  34554  ballotlemrinv  34716  hgt750lem2  34834  bnj1146  34971  bnj893  35108  bnj1234  35193  r11  35275  r12  35276  subfacp1lem1  35399  kur14lem2  35427  kur14lem5  35430  kur14lem7  35432  cvmscld  35493  satfv1lem  35582  fmla0  35602  mvtval  35720  mthmpps  35802  fixun  36127  rabeqbii  36414  iuneq12i  36415  iineq1i  36416  iineq12i  36417  riotaeqbii  36418  ixpeq1i  36420  sumeq2si  36422  prodeq2si  36424  itgeq12i  36426  ditgeq123i  36429  cbvcsbvw2  36451  cbviunvw2  36452  cbviinvw2  36453  cbvmptvw2  36454  cbvriotavw2  36456  cbvoprab1vw  36457  cbvoprab2vw  36458  cbvoprab123vw  36459  cbvoprab23vw  36460  cbvoprab13vw  36461  cbvmpovw2  36462  cbvmpo1vw2  36463  cbvmpo2vw2  36464  cbvixpvw2  36465  cbvprodvw2  36467  cbvitgvw2  36468  cbvditgvw2  36469  bj-inrab  37179  bj-inrab3  37181  bj-gabeqis  37190  bj-pr1un  37255  bj-pr2un  37269  bj-dfid2ALT  37317  bj-mpomptALT  37376  rnmptsn  37594  f1omptsnlem  37595  rabiun  37848  phpreu  37859  poimirlem18  37893  ovoliunnfl  37917  voliunnfl  37919  mbfposadd  37922  asindmre  37958  abeqin  38509  rncnvepres  38564  qsresid  38586  dmxrn  38642  rnxrn  38676  xrnres  38680  xrnres2  38681  xrnres3  38682  dmxrncnvepres2  38688  dfsucmap3  38718  dfsucmap2  38719  rncossdmcoss  38800  1cosscnvxrn  38820  refrelsredund4  38971  mpets  39211  dfpetparts2  39227  dfpeters2  39229  petseq  39231  pets2eq  39232  cdleme25cv  40738  sn-iotalemcor  42598  sqdeccom12  42663  sumcubes  42687  resuppsinopn  42737  sn-00idlem2  42773  sn-1ticom  42809  mendsca  43546  areaquad  43577  onsucrn  43632  df3o2  43674  df3o3  43675  omcl3g  43695  dfno2  43788  cnvrcl0  43985  sqrtcvallem1  43991  trclrelexplem  44071  iuneq1i  45448  cbvmpo2  45460  cbvmpo1  45461  cbvrabv2w  45491  mptssid  45603  fprodabs2  45959  stoweidlem13  46375  wallispilem4  46430  fourierdlem94  46562  fourierdlem102  46570  fourierdlem111  46579  fourierdlem112  46580  fourierdlem113  46581  fourierdlem114  46582  41prothprmlem2  47982  2exp340mod341  48097  8exp8mod9  48100  nfermltl8rev  48106  stgr1  48325  gpgprismgr4cycllem6  48464  gpgprismgr4cycllem9  48467  gpgprismgr4cycllem10  48468  cbvmpox2  48700  dmmpossx2  48701  zlmodzxzequa  48860  zlmodzxzequap  48863  resinsn  49235  dfswapf2  49624