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

Theorem 3eqtr4i 2683
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 2676 . 2 𝐷 = 𝐴
51, 4eqtr4i 2676 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  rabrab  3146  rabswap  3151  rabbiia  3215  cbvrab  3229  cbvcsb  3571  csbco  3576  cbvrabcsf  3601  un4  3806  in13  3859  in31  3860  in4  3862  symdifcom  3878  indifcom  3905  indir  3908  undir  3909  difdif2  3917  notrab  3937  dfnul3  3951  rab0OLD  3989  dfif5  4135  rabsnifsb  4289  prcom  4299  tprot  4316  tpcoma  4317  tpcomb  4318  tpass  4319  qdassr  4321  pw0  4375  pwpw0  4376  pwsn  4460  pwsnALT  4461  int0OLD  4523  cbviun  4589  cbviin  4590  iunrab  4599  iunin1  4617  iinuni  4641  cbvopab  4754  cbvopab1  4756  cbvopab2  4757  cbvopab1s  4758  cbvopab2v  4760  unopab  4761  cbvmptf  4781  cbvmpt  4782  iunopab  5041  dfid3  5054  dfid4  5055  rabxp  5188  fconstmpt  5197  csbxp  5234  inxp  5287  cnvco  5340  csbdm  5350  rnmpt  5403  csbres  5431  resundi  5445  resundir  5446  resindi  5447  resindir  5448  rescom  5458  resima  5466  imadmrn  5511  cnvimarndm  5521  cnvi  5572  cnvin  5575  rnun  5576  imaundi  5580  cnvxp  5586  imainrect  5610  csbrn  5631  imacnvcnv  5634  resdmres  5663  imadmres  5665  mptpreima  5666  dfpred3  5728  predin  5741  predun  5742  preddif  5743  wfi  5751  cbviota  5894  sb8iota  5896  resdif  6195  opabiotadm  6299  fndmin  6364  fninfp  6481  cbvriota  6661  dfoprab2  6743  cbvoprab1  6769  cbvoprab2  6770  cbvoprab12  6771  cbvoprab3  6773  cbvmpt2x  6775  resoprab  6798  caov32  6903  caov31  6905  caov4  6907  caovlem2  6912  uniuni  7013  zfrep6  7176  ofmres  7206  dfopab2  7266  dfxp3  7275  dmmpt2ssx  7280  fmpt2x  7281  fsplit  7327  ovtpos  7412  tposco  7428  tfrlem10  7528  o2p2e4  7666  mapsncnv  7946  cbvixp  7967  xpcomco  8091  sbthlem6  8116  1sdom  8204  cardf2  8807  alephcard  8931  alephfplem1  8965  pwcda1  9054  ackbij1lem14  9093  compsscnv  9231  dffin1-5  9248  ituniiun  9282  axdc2lem  9308  axdc3lem4  9313  axcclem  9317  pwcfsdom  9443  dmaddpi  9750  dmmulpi  9751  adderpqlem  9814  addassnq  9818  mulcanenq  9820  addcmpblnr  9928  mulcmpblnrlem  9929  ltsrpr  9936  mulgt0sr  9964  sqgt0sr  9965  axi2m1  10018  negiso  11041  nummac  11596  decsubi  11621  decsubiOLD  11622  9t11e99  11709  9t11e99OLD  11710  fzprval  12439  fztpval  12440  seqval  12852  sqrecii  12986  sqdivi  12988  binom2i  13014  4bc2eq6  13156  hashgval  13160  revs1  13560  cats1cat  13652  trclublem  13780  shftdm  13855  shftidt2  13865  cji  13943  cbvsum  14469  sumfc  14484  ackbijnn  14604  cbvprod  14689  prodfc  14719  fsumcube  14835  divalglem2  15165  nn0gcdsq  15507  prmreclem2  15668  prmrec  15673  hashbc0  15756  dec5nprm  15817  dec2nprm  15818  gcdi  15824  decexp2  15826  decsplit  15834  decsplitOLD  15838  1259lem1  15885  1259lem4  15888  4001lem1  15895  dfpleOLD  16009  strlemor2OLD  16017  strlemor3OLD  16018  phlstr  16081  lubdm  17026  glbdm  17039  oduval  17177  oduleval  17178  odubas  17180  oppgid  17832  symgbas0  17860  gsumcom2  18420  ringidval  18549  oppr1  18680  dfrhm2  18765  rmodislmod  18979  opsrtoslem1  19532  cnfldsub  19822  cnflddiv  19824  dvdsrzring  19879  pjdm  20099  pjfval2  20101  restco  21016  cnmptid  21512  ufprim  21760  tgioo3  22655  oprpiece1res1  22797  oprpiece1res2  22798  volfiniun  23361  vitalilem4  23425  cbvitg  23587  itgresr  23590  iblcnlem1  23599  cbvditg  23663  sincos3rdpi  24313  logblog  24575  ang180lem2  24585  1cubrlem  24613  asin1  24666  log2ublem2  24719  log2ublem3  24720  emcllem5  24771  lgsdir2lem5  25099  lgsquadlem3  25152  2lgslem1b  25162  2lgsoddprmlem3d  25183  cchhllem  25812  ax5seglem7  25860  axlowdimlem4  25870  vtxval0  25976  iedgval0  25977  finsumvtxdg2ssteplem1  26497  1wlkdlem1  27115  ex-un  27411  ex-pw  27416  ex-cnv  27424  ex-co  27425  bafval  27587  vsfval  27616  cnnvba  27662  cnnvm  27665  ip2dii  27827  siilem1  27834  h2hcau  27964  hvsubsub4i  28044  hvnegdii  28047  normlem3  28097  normlem8  28102  norm-iii-i  28124  normpar2i  28141  polid2i  28142  chjassi  28473  chj4i  28510  h1de2i  28540  spanunsni  28566  fh3i  28610  fh4i  28611  qlax4i  28617  qlaxr3i  28623  3oalem5  28653  pjadjii  28661  pjsubii  28665  hoadd32i  28765  cnvadj  28879  hh0oi  28890  hhcno  28891  hhcnf  28892  nmopnegi  28952  lnophmlem2  29004  branmfn  29092  abrexexd  29473  cbviunf  29498  maprnin  29634  dpmul10  29731  dpexpp1  29744  dpadd3  29748  dpmul  29749  dpmul4  29750  psgnfzto1st  29983  lmlimxrge0  30122  rrhre  30193  cbvesum  30232  unibrsiga  30377  eulerpartlemt  30561  eulerpartgbij  30562  ballotlem2  30678  ballotlemrinv  30723  hgt750lem2  30858  bnj1146  30988  bnj893  31124  bnj1234  31207  subfacp1lem1  31287  kur14lem2  31315  kur14lem5  31318  kur14lem7  31320  cvmscld  31381  mvtval  31523  mthmpps  31605  frpoind  31865  frind  31868  frrlem7  31915  frrlem10  31916  noextend  31944  nosupbday  31976  nosupbnd1  31985  nosupbnd2  31987  dmscut  32043  madeval2  32061  fixun  32141  bj-inrab  33048  bj-inrab3  33050  bj-pr1un  33116  bj-pr2un  33130  bj-mpt2mptALT  33197  f1omptsnlem  33313  rabiun  33512  phpreu  33523  poimirlem18  33557  ovoliunnfl  33581  voliunnfl  33583  mbfposadd  33587  asindmre  33625  abeqin  34158  rncnvepres  34214  qsresid  34237  rnxrn  34296  xrnres  34300  xrnres2  34301  xrnres3  34302  rncossdmcoss  34345  1cosscnvxrn  34365  cdleme25cv  35963  mendsca  38076  areaquad  38119  cnvrcl0  38249  trclrelexplem  38320  df3o2  38639  df3o3  38640  cbvmpt22  39591  cbvmpt21  39592  mptssid  39764  fprodabs2  40145  stoweidlem13  40548  wallispilem4  40603  fourierdlem94  40735  fourierdlem102  40743  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fourierdlem114  40755  41prothprmlem2  41860  cbvmpt2x2  42439  dmmpt2ssx2  42440  zlmodzxzequa  42610  zlmodzxzequap  42613
  Copyright terms: Public domain W3C validator