MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr4i Structured version   Visualization version   GIF version

Theorem 3eqtr4i 2849
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
StepHypRef Expression
1 3eqtr4i.2 . 2 𝐶 = 𝐴
2 3eqtr4i.3 . . 3 𝐷 = 𝐵
3 3eqtr4i.1 . . 3 𝐴 = 𝐵
42, 3eqtr4i 2842 . 2 𝐷 = 𝐴
51, 4eqtr4i 2842 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2810
This theorem is referenced by:  rabrab  3316  rabswap  3321  rabbiia  3385  cbvrab  3399  cbvcsb  3744  csbco  3749  cbvrabcsf  3774  un4  3983  in13  4034  in31  4035  in4  4037  symdifcom  4054  indifcom  4085  indir  4088  undir  4089  difdif2  4097  notrab  4116  dfnul3  4130  dfif5  4306  rabsnifsb  4459  prcom  4469  tprot  4486  tpcoma  4487  tpcomb  4488  tpass  4489  qdassr  4491  pw0  4544  pwpw0  4545  pwsn  4633  pwsnALT  4634  cbviun  4760  cbviin  4761  iunrab  4770  iunin1  4788  iinuni  4812  cbvopab  4926  cbvopab1  4928  cbvopab2  4929  cbvopab1s  4930  cbvopab2v  4932  unopab  4933  cbvmptf  4953  cbvmpt  4954  iunopab  5220  dfid3  5233  dfid4  5234  rabxp  5367  fconstmpt  5376  csbxp  5415  inxp  5469  cnvco  5522  csbdm  5532  rnmpt  5585  csbres  5613  resundi  5627  resundir  5628  resindi  5629  resindir  5630  rescom  5639  resima  5647  imadmrn  5699  cnvimarndm  5709  cnvi  5761  cnvin  5764  rnun  5765  imaundi  5769  cnvxp  5775  imainrect  5799  csbrn  5820  imacnvcnv  5823  resdmres  5852  imadmres  5854  mptpreima  5855  dfpred3  5916  predin  5929  predun  5930  preddif  5931  wfi  5939  cbviota  6078  sb8iota  6080  resdif  6382  opabiotadm  6490  fndmin  6555  fninfp  6674  cbvriota  6854  dfoprab2  6940  cbvoprab1  6966  cbvoprab2  6967  cbvoprab12  6968  cbvoprab3  6970  cbvmpt2x  6972  resoprab  6995  caov32  7100  caov31  7102  caov4  7104  caovlem2  7109  uniuni  7210  zfrep6  7373  ofmres  7403  dfopab2  7463  dfxp3  7472  dmmpt2ssx  7477  fmpt2x  7478  fsplit  7525  ovtpos  7611  tposco  7627  tfrlem10  7728  o2p2e4  7867  mapsncnv  8150  cbvixp  8171  xpcomco  8298  sbthlem6  8323  1sdom  8411  cardf2  9061  alephcard  9185  alephfplem1  9219  pwcda1  9310  ackbij1lem14  9349  compsscnv  9487  dffin1-5  9504  ituniiun  9538  axdc2lem  9564  axdc3lem4  9569  axcclem  9573  pwcfsdom  9699  dmaddpi  10006  dmmulpi  10007  adderpqlem  10070  addassnq  10074  mulcanenq  10076  addcmpblnr  10184  mulcmpblnrlem  10185  ltsrpr  10192  mulgt0sr  10220  sqgt0sr  10221  axi2m1  10274  negiso  11297  nummac  11823  decsubi  11841  9t11e99  11908  fzprval  12643  fztpval  12644  seqval  13054  sqrecii  13188  sqdivi  13190  binom2i  13216  4bc2eq6  13355  hashgval  13359  revs1  13757  cats1cat  13849  trclublem  13978  shftdm  14053  shftidt2  14063  cji  14141  cbvsum  14667  sumfc  14682  ackbijnn  14801  cbvprod  14885  prodfc  14915  fsumcube  15030  divalglem2  15357  nn0gcdsq  15696  prmreclem2  15857  prmrec  15862  hashbc0  15945  dec5nprm  16006  dec2nprm  16007  gcdi  16013  decexp2  16015  decsplit  16023  1259lem1  16068  1259lem4  16071  4001lem1  16078  strlemor2OLD  16200  strlemor3OLD  16201  phlstr  16264  lubdm  17203  glbdm  17216  oduval  17354  oduleval  17355  odubas  17357  oppgid  18006  symgbas0  18034  gsumcom2  18594  ringidval  18724  oppr1  18855  dfrhm2  18940  rmodislmod  19154  opsrtoslem1  19711  cnfldsub  20001  cnflddiv  20003  dvdsrzring  20058  pjdm  20281  pjfval2  20283  restco  21202  cnmptid  21698  ufprim  21946  tgioo3  22841  oprpiece1res1  22983  oprpiece1res2  22984  volfiniun  23550  vitalilem4  23614  cbvitg  23778  itgresr  23781  iblcnlem1  23790  cbvditg  23854  sincos3rdpi  24505  logblog  24766  ang180lem2  24776  1cubrlem  24804  asin1  24857  log2ublem2  24910  log2ublem3  24911  emcllem5  24962  lgsdir2lem5  25290  lgsquadlem3  25343  2lgslem1b  25353  2lgsoddprmlem3d  25374  cchhllem  26003  ax5seglem7  26051  axlowdimlem4  26061  vtxval0  26167  iedgval0  26168  finsumvtxdg2ssteplem1  26691  1wlkdlem1  27332  ex-un  27634  ex-pw  27639  ex-cnv  27647  ex-co  27648  bafval  27809  vsfval  27838  cnnvba  27884  cnnvm  27887  ip2dii  28049  siilem1  28056  h2hcau  28186  hvsubsub4i  28266  hvnegdii  28269  normlem3  28319  normlem8  28324  norm-iii-i  28346  normpar2i  28363  polid2i  28364  chjassi  28695  chj4i  28732  h1de2i  28762  spanunsni  28788  fh3i  28832  fh4i  28833  qlax4i  28839  qlaxr3i  28845  3oalem5  28875  pjadjii  28883  pjsubii  28887  hoadd32i  28987  cnvadj  29101  hh0oi  29112  hhcno  29113  hhcnf  29114  nmopnegi  29174  lnophmlem2  29226  branmfn  29314  abrexexd  29694  cbviunf  29719  maprnin  29855  dpmul10  29950  dpexpp1  29963  dpadd3  29967  dpmul  29968  dpmul4  29969  psgnfzto1st  30202  lmlimxrge0  30341  rrhre  30412  cbvesum  30451  unibrsiga  30596  eulerpartlemt  30780  eulerpartgbij  30781  ballotlem2  30897  ballotlemrinv  30942  hgt750lem2  31077  bnj1146  31206  bnj893  31342  bnj1234  31425  subfacp1lem1  31505  kur14lem2  31533  kur14lem5  31536  kur14lem7  31538  cvmscld  31599  mvtval  31741  mthmpps  31823  frpoind  32082  frind  32085  frrlem7  32132  frrlem10  32133  noextend  32161  nosupbday  32193  nosupbnd1  32202  nosupbnd2  32204  dmscut  32260  madeval2  32278  fixun  32358  bj-inrab  33252  bj-inrab3  33254  bj-pr1un  33319  bj-pr2un  33333  bj-mpt2mptALT  33401  f1omptsnlem  33518  rabiun  33713  phpreu  33724  poimirlem18  33758  ovoliunnfl  33782  voliunnfl  33784  mbfposadd  33787  asindmre  33825  abeqin  34353  rncnvepres  34407  qsresid  34429  rnxrn  34487  xrnres  34491  xrnres2  34492  xrnres3  34493  rncossdmcoss  34536  1cosscnvxrn  34556  cdleme25cv  36156  mendsca  38277  areaquad  38319  cnvrcl0  38449  trclrelexplem  38520  df3o2  38839  df3o3  38840  cbvmpt22  39787  cbvmpt21  39788  mptssid  39951  fprodabs2  40324  stoweidlem13  40726  wallispilem4  40781  fourierdlem94  40913  fourierdlem102  40921  fourierdlem111  40930  fourierdlem112  40931  fourierdlem113  40932  fourierdlem114  40933  41prothprmlem2  42127  cbvmpt2x2  42699  dmmpt2ssx2  42700  zlmodzxzequa  42870  zlmodzxzequap  42873
  Copyright terms: Public domain W3C validator