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

Theorem 3eqtr4i 2642
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 2635 . 2 𝐷 = 𝐴
51, 4eqtr4i 2635 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  rabswap  3098  rabbiia  3161  cbvrab  3171  cbvcsb  3504  csbco  3509  cbvrabcsf  3534  un4  3735  in13  3788  in31  3789  in4  3791  symdifcom  3807  indifcom  3831  indir  3834  undir  3835  difdif2  3843  notrab  3863  dfnul3  3877  rab0OLD  3910  dfif5  4052  rabsnifsb  4201  prcom  4211  tprot  4228  tpcoma  4229  tpcomb  4230  tpass  4231  qdassr  4233  pw0  4283  pwpw0  4284  pwsn  4361  pwsnALT  4362  int0OLD  4421  rabasiun  4454  cbviun  4488  cbviin  4489  iunrab  4498  iunin1  4516  iinuni  4540  cbvopab  4648  cbvopab1  4650  cbvopab2  4651  cbvopab1s  4652  cbvopab2v  4654  unopab  4655  cbvmptf  4671  cbvmpt  4672  iunopab  4926  dfid3  4944  dfid4  4945  rabxp  5068  fconstmpt  5075  csbxp  5113  inxp  5164  cnvco  5218  csbdm  5227  rnmpt  5279  csbres  5307  resundi  5317  resundir  5318  resindi  5319  resindir  5320  rescom  5330  resima  5338  imadmrn  5382  cnvimarndm  5392  cnvi  5442  cnvin  5445  rnun  5446  imaundi  5450  cnvxp  5456  imainrect  5480  csbrn  5500  imacnvcnv  5503  resdmres  5529  imadmres  5530  mptpreima  5531  dfpred3  5593  predin  5606  predun  5607  preddif  5608  wfi  5616  cbviota  5759  sb8iota  5761  resdif  6055  opabiotadm  6155  fndmin  6217  fninfp  6323  cbvriota  6499  dfoprab2  6577  cbvoprab1  6603  cbvoprab2  6604  cbvoprab12  6605  cbvoprab3  6607  cbvmpt2x  6609  resoprab  6632  caov32  6737  caov31  6739  caov4  6741  caovlem2  6746  uniuni  6843  zfrep6  7005  ofmres  7033  dfopab2  7091  dfxp3  7097  dmmpt2ssx  7102  fmpt2x  7103  fsplit  7147  ovtpos  7232  tposco  7248  tfrlem10  7348  o2p2e4  7486  mapsncnv  7768  cbvixp  7789  xpcomco  7913  sbthlem6  7938  1sdom  8026  cardf2  8630  alephcard  8754  alephfplem1  8788  pwcda1  8877  ackbij1lem14  8916  compsscnv  9054  dffin1-5  9071  ituniiun  9105  axdc2lem  9131  axdc3lem4  9136  axcclem  9140  pwcfsdom  9262  dmaddpi  9569  dmmulpi  9570  adderpqlem  9633  addassnq  9637  mulcanenq  9639  addcmpblnr  9747  mulcmpblnrlem  9748  ltsrpr  9755  mulgt0sr  9783  sqgt0sr  9784  axi2m1  9837  negiso  10853  nummac  11393  decsubi  11418  decsubiOLD  11419  9t11e99  11506  9t11e99OLD  11507  fzprval  12229  fztpval  12230  seqval  12632  sqrecii  12766  sqdivi  12768  binom2i  12794  4bc2eq6  12936  hashgval  12940  revs1  13314  cats1cat  13406  trclublem  13531  shftdm  13608  shftidt2  13618  cji  13696  cbvsum  14222  sumfc  14236  ackbijnn  14348  cbvprod  14433  prodfc  14463  fsumcube  14579  divalglem2  14905  nn0gcdsq  15247  prmreclem2  15408  prmrec  15413  hashbc0  15496  dec5nprm  15557  dec2nprm  15558  gcdi  15564  decexp2  15566  decsplit  15574  decsplitOLD  15578  1259lem1  15625  1259lem4  15628  4001lem1  15635  dfpleOLD  15738  strlemor2  15746  strlemor3  15747  phlstr  15806  lubdm  16751  glbdm  16764  oduval  16902  oduleval  16903  odubas  16905  oppgid  17558  symgbas0  17586  gsumcom2  18146  ringidval  18275  oppr1  18406  dfrhm2  18489  opsrtoslem1  19254  cnfldsub  19542  cnflddiv  19544  dvdsrzring  19599  pjdm  19818  pjfval2  19820  restco  20726  cnmptid  21222  ufprim  21471  tgioo3  22364  oprpiece1res1  22506  oprpiece1res2  22507  volfiniun  23067  vitalilem4  23131  cbvitg  23293  itgresr  23296  iblcnlem1  23305  cbvditg  23369  sincos3rdpi  24017  logblog  24275  ang180lem2  24285  1cubrlem  24313  asin1  24366  log2ublem2  24419  log2ublem3  24420  emcllem5  24471  lgsdir2lem5  24799  lgsquadlem3  24852  2lgslem1b  24862  2lgsoddprmlem3d  24883  cchhllem  25513  ax5seglem7  25561  axlowdimlem4  25571  usgraop  25673  usgrafilem1  25734  cusgrasizeindslem1  25796  vdgrun  26222  vdgrfiun  26223  vdegp1bi  26306  konigsberg  26308  ex-un  26467  ex-pw  26472  ex-cnv  26480  ex-co  26481  bafval  26637  vsfval  26666  cnnvba  26712  cnnvm  26715  ip2dii  26877  siilem1  26884  h2hcau  27014  hvsubsub4i  27094  hvnegdii  27097  normlem3  27147  normlem8  27152  norm-iii-i  27174  normpar2i  27191  polid2i  27192  chjassi  27523  chj4i  27560  h1de2i  27590  spanunsni  27616  fh3i  27660  fh4i  27661  qlax4i  27667  qlaxr3i  27673  3oalem5  27703  pjadjii  27711  pjsubii  27715  hoadd32i  27815  cnvadj  27929  hh0oi  27940  hhcno  27941  hhcnf  27942  nmopnegi  28002  lnophmlem2  28054  branmfn  28142  rabrab  28516  abrexexd  28525  cbviunf  28549  maprnin  28688  psgnfzto1st  28980  lmlimxrge0  29116  rrhre  29187  cbvesum  29225  unibrsiga  29370  eulerpartlemt  29554  eulerpartgbij  29555  ballotlem2  29671  ballotlemrinv  29716  bnj1146  29910  bnj893  30046  bnj1234  30129  subfacp1lem1  30209  kur14lem2  30237  kur14lem5  30240  kur14lem7  30242  cvmscld  30303  mvtval  30445  mthmpps  30527  frind  30778  fixun  30980  bj-inrab  31909  bj-pr1un  31978  bj-pr2un  31992  bj-mpt2mptALT  32047  f1omptsnlem  32153  rabiun  32346  phpreu  32357  poimirlem18  32391  ovoliunnfl  32415  voliunnfl  32417  mbfposadd  32421  asindmre  32459  cdleme25cv  34458  mendsca  36572  areaquad  36615  cnvrcl0  36745  trclrelexplem  36816  df3o2  37136  df3o3  37137  cbvmpt22  38099  cbvmpt21  38100  fprodabs2  38456  stoweidlem13  38700  wallispilem4  38755  fourierdlem94  38887  fourierdlem102  38895  fourierdlem111  38904  fourierdlem112  38905  fourierdlem113  38906  fourierdlem114  38907  41prothprmlem2  39868  vtxval0  40262  iedgval0  40263  11wlkdlem1  41296  cbvmpt2x2  41899  dmmpt2ssx2  41900  zlmodzxzequa  42071  zlmodzxzequap  42074
  Copyright terms: Public domain W3C validator