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

Theorem 3eqtr4i 2858
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 2851 . 2 𝐷 = 𝐴
51, 4eqtr4i 2851 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818
This theorem is referenced by:  rabrab  3384  rabbiia  3477  cbvrabw  3494  cbvrab  3495  cbvrabv  3496  cbvcsbw  3896  cbvcsb  3897  csbcow  3901  csbco  3902  cbvrabcsfw  3927  cbvrabcsf  3931  un4  4148  incom  4181  in13  4202  in31  4203  in4  4205  symdifcom  4223  indifcom  4252  indir  4255  undir  4256  difdif2  4264  notrab  4283  dfnul3  4298  dfif5  4485  rabsnifsb  4656  prcom  4666  tprot  4683  tpcoma  4684  tpcomb  4685  tpass  4686  qdassr  4688  pw0  4743  pwpw0  4744  pwsn  4828  pwsnALT  4829  cbviun  4957  cbviin  4958  cbviung  4959  cbviing  4960  iunrab  4972  iunin1  4990  iinuni  5016  cbvopab  5133  cbvopab1  5135  cbvopab1g  5136  cbvopab2  5137  cbvopab1s  5138  cbvopab2v  5140  unopab  5141  cbvmptf  5161  cbvmptfg  5162  iunopab  5442  dfid4  5459  dfid3  5460  rabxp  5598  fconstmpt  5612  csbxp  5648  inxp  5701  cnvco  5754  csbdm  5764  rnmpt  5825  csbres  5854  resundi  5865  resundir  5866  resindi  5867  resindir  5868  rescom  5877  resima  5885  imadmrn  5936  cnvimarndm  5947  cnvi  5997  cnvin  6000  rnun  6001  imaundi  6005  cnvxp  6011  imainrect  6035  csbrn  6057  imacnvcnv  6060  resdmres  6086  imadmres  6088  mptpreima  6089  dfpred3  6155  predin  6168  predun  6169  preddif  6170  wfi  6178  cbviotaw  6318  cbviota  6320  sb8iota  6322  resdif  6631  opabiotadm  6741  fndmin  6810  fninfp  6931  cbvriotaw  7118  cbvriota  7122  dfoprab2  7207  cbvoprab1  7234  cbvoprab2  7235  cbvoprab12  7236  cbvoprab3  7238  cbvmpox  7240  resoprab  7263  caov32  7368  caov31  7370  caov4  7372  caovlem2  7377  uniuni  7476  zfrep6  7650  ofmres  7679  dfopab2  7744  dfxp3  7753  dmmpossx  7758  fmpox  7759  fsplit  7806  fsplitOLD  7807  ovtpos  7901  tposco  7917  tfrlem10  8017  o2p2e4  8160  mapsncnv  8449  cbvixp  8470  xpcomco  8599  sbthlem6  8624  1sdom  8713  cardf2  9364  alephcard  9488  alephfplem1  9522  xp2dju  9594  djuassen  9596  infdju1  9607  pwdju1  9608  ackbij1lem14  9647  compsscnv  9785  dffin1-5  9802  ituniiun  9836  axdc2lem  9862  axdc3lem4  9867  axcclem  9871  pwcfsdom  9997  dmaddpi  10304  dmmulpi  10305  adderpqlem  10368  addassnq  10372  mulcanenq  10374  addcmpblnr  10483  mulcmpblnrlem  10484  ltsrpr  10491  mulgt0sr  10519  sqgt0sr  10520  axi2m1  10573  negiso  11613  nummac  12135  decsubi  12153  9t11e99  12220  fztpval  12962  seqval  13373  sqrecii  13539  sqdivi  13541  binom2i  13567  4bc2eq6  13682  hashgval  13686  revs1  14120  cats1cat  14216  trclublem  14348  shftdm  14423  shftidt2  14433  cji  14511  cbvsum  15044  sumfc  15058  ackbijnn  15175  cbvprod  15261  prodfc  15291  fsumcube  15406  divalglem2  15738  nn0gcdsq  16084  prmreclem2  16245  prmrec  16250  hashbc0  16333  dec5nprm  16394  dec2nprm  16395  gcdi  16401  decexp2  16403  decsplit  16411  1259lem1  16456  1259lem4  16459  4001lem1  16466  phlstr  16645  lubdm  17581  glbdm  17594  oduval  17732  oduleval  17733  odubas  17735  oppgid  18416  symgbas0  18444  gsumcom2  19017  ringidval  19175  oppr1  19306  dfrhm2  19391  rmodislmod  19624  opsrtoslem1  20184  cnfldsub  20491  cnflddiv  20493  dvdsrzring  20548  pjdm  20769  pjfval2  20771  restco  21690  ufprim  22435  tgioo3  23330  oprpiece1res1  23472  oprpiece1res2  23473  volfiniun  24065  vitalilem4  24129  cbvitg  24293  itgresr  24296  cbvditg  24369  plyid  24716  coeidp  24770  dgrid  24771  sincos3rdpi  25019  logblog  25285  ang180lem2  25303  1cubrlem  25334  asin1  25387  log2ublem2  25441  log2ublem3  25442  emcllem5  25493  lgsdir2lem5  25821  lgsquadlem3  25874  2lgslem1b  25884  2lgsoddprmlem3d  25905  cchhllem  26589  ax5seglem7  26637  vtxval0  26740  iedgval0  26741  finsumvtxdg2ssteplem1  27243  wwlksnfi  27600  1wlkdlem1  27832  ex-un  28119  ex-pw  28124  ex-cnv  28132  ex-co  28133  bafval  28297  vsfval  28326  cnnvba  28372  cnnvm  28375  ip2dii  28537  siilem1  28544  h2hcau  28672  hvsubsub4i  28752  hvnegdii  28755  normlem3  28805  normlem8  28810  norm-iii-i  28832  normpar2i  28849  polid2i  28850  chjassi  29179  chj4i  29216  h1de2i  29246  spanunsni  29272  fh3i  29316  fh4i  29317  qlax4i  29323  qlaxr3i  29329  3oalem5  29359  pjadjii  29367  pjsubii  29371  hoadd32i  29471  cnvadj  29585  hh0oi  29596  hhcno  29597  hhcnf  29598  nmopnegi  29658  lnophmlem2  29710  branmfn  29798  dmrab  30176  abrexexd  30185  cbviunf  30224  maprnin  30382  dpmul10  30487  dpexpp1  30500  dpadd3  30504  dpmul  30505  dpmul4  30506  psgnfzto1st  30663  cycpmconjs  30714  lmlimxrge0  31079  zrhre  31148  qqhre  31149  rrhre  31150  cbvesum  31189  unibrsiga  31333  eulerpartlemt  31517  eulerpartgbij  31518  ballotlemrinv  31679  hgt750lem2  31811  bnj1146  31951  bnj893  32088  bnj1234  32171  subfacp1lem1  32312  kur14lem2  32340  kur14lem5  32343  kur14lem7  32345  cvmscld  32406  satfv1lem  32495  fmla0  32515  mvtval  32633  mthmpps  32715  frpoind  32966  frind  32971  frrlem5  33013  noextend  33059  nosupbday  33091  nosupbnd1  33100  nosupbnd2  33102  dmscut  33158  madeval2  33176  fixun  33256  bj-inrab  34131  bj-inrab3  34133  bj-pr1un  34201  bj-pr2un  34215  bj-mpomptALT  34292  rnmptsn  34487  f1omptsnlem  34488  rabiun  34734  phpreu  34745  poimirlem18  34779  ovoliunnfl  34803  voliunnfl  34805  mbfposadd  34808  asindmre  34846  abeqin  35384  rncnvepres  35431  qsresid  35452  rnxrn  35515  xrnres  35519  xrnres2  35520  xrnres3  35521  rncossdmcoss  35564  1cosscnvxrn  35584  refrelsredund4  35736  cdleme25cv  37363  sqdeccom12  39042  nn0expgcd  39051  sn-00idlem2  39096  mendsca  39656  areaquad  39690  cnvrcl0  39852  trclrelexplem  39923  df3o2  40241  df3o3  40242  cbvmpo2  41230  cbvmpo1  41231  mptssid  41378  fprodabs2  41743  stoweidlem13  42166  wallispilem4  42221  fourierdlem94  42353  fourierdlem102  42361  fourierdlem111  42370  fourierdlem112  42371  fourierdlem113  42372  fourierdlem114  42373  41prothprmlem2  43617  2exp340mod341  43732  8exp8mod9  43735  nfermltl8rev  43741  cbvmpox2  44218  dmmpossx2  44219  zlmodzxzequa  44385  zlmodzxzequap  44388
  Copyright terms: Public domain W3C validator