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

Theorem 3eqtr4i 2854
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 2847 . 2 𝐷 = 𝐴
51, 4eqtr4i 2847 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  rabrab  3380  rabbiia  3473  cbvrabw  3490  cbvrab  3491  cbvrabv  3492  cbvcsbw  3892  cbvcsb  3893  csbcow  3897  csbco  3898  cbvrabcsfw  3923  cbvrabcsf  3927  un4  4144  incom  4177  in13  4198  in31  4199  in4  4201  symdifcom  4219  indifcom  4248  indir  4251  undir  4252  difdif2  4260  notrab  4279  dfnul3  4294  dfif5  4481  rabsnifsb  4652  prcom  4662  tprot  4679  tpcoma  4680  tpcomb  4681  tpass  4682  qdassr  4684  pw0  4739  pwpw0  4740  pwsn  4824  pwsnALT  4825  cbviun  4953  cbviin  4954  cbviung  4955  cbviing  4956  iunrab  4968  iunin1  4986  iinuni  5012  cbvopab  5129  cbvopab1  5131  cbvopab1g  5132  cbvopab2  5133  cbvopab1s  5134  cbvopab2v  5136  unopab  5137  cbvmptf  5157  cbvmptfg  5158  iunopab  5438  dfid4  5455  dfid3  5456  rabxp  5594  fconstmpt  5608  csbxp  5644  inxp  5697  cnvco  5750  csbdm  5760  rnmpt  5821  csbres  5850  resundi  5861  resundir  5862  resindi  5863  resindir  5864  rescom  5873  resima  5881  imadmrn  5933  cnvimarndm  5944  cnvi  5994  cnvin  5997  rnun  5998  imaundi  6002  cnvxp  6008  imainrect  6032  csbrn  6054  imacnvcnv  6057  resdmres  6083  imadmres  6085  mptpreima  6086  dfpred3  6152  predin  6165  predun  6166  preddif  6167  wfi  6175  cbviotaw  6315  cbviota  6317  sb8iota  6319  resdif  6629  opabiotadm  6739  fndmin  6808  fninfp  6929  cbvriotaw  7112  cbvriota  7116  dfoprab2  7201  cbvoprab1  7230  cbvoprab2  7231  cbvoprab12  7232  cbvoprab3  7234  cbvmpox  7236  resoprab  7259  caov32  7364  caov31  7366  caov4  7368  caovlem2  7373  uniuni  7472  zfrep6  7647  ofmres  7676  dfopab2  7741  dfxp3  7750  dmmpossx  7755  fmpox  7756  fsplit  7803  fsplitOLD  7804  ovtpos  7898  tposco  7914  tfrlem10  8014  o2p2e4  8157  mapsncnv  8446  cbvixp  8467  xpcomco  8596  sbthlem6  8621  1sdom  8710  cardf2  9361  alephcard  9485  alephfplem1  9519  xp2dju  9591  djuassen  9593  infdju1  9604  pwdju1  9605  ackbij1lem14  9644  compsscnv  9782  dffin1-5  9799  ituniiun  9833  axdc2lem  9859  axdc3lem4  9864  axcclem  9868  pwcfsdom  9994  dmaddpi  10301  dmmulpi  10302  adderpqlem  10365  addassnq  10369  mulcanenq  10371  addcmpblnr  10480  mulcmpblnrlem  10481  ltsrpr  10488  mulgt0sr  10516  sqgt0sr  10517  axi2m1  10570  negiso  11610  nummac  12132  decsubi  12150  9t11e99  12217  fztpval  12959  seqval  13370  sqrecii  13536  sqdivi  13538  binom2i  13564  4bc2eq6  13679  hashgval  13683  revs1  14117  cats1cat  14213  trclublem  14345  shftdm  14420  shftidt2  14430  cji  14508  cbvsum  15042  sumfc  15056  ackbijnn  15173  cbvprod  15259  prodfc  15289  fsumcube  15404  divalglem2  15736  nn0gcdsq  16082  prmreclem2  16243  prmrec  16248  hashbc0  16331  dec5nprm  16392  dec2nprm  16393  gcdi  16399  decexp2  16401  decsplit  16409  1259lem1  16454  1259lem4  16457  4001lem1  16464  phlstr  16643  lubdm  17579  glbdm  17592  oduval  17730  oduleval  17731  odubas  17733  oppgid  18424  symgbas0  18453  gsumcom2  19026  ringidval  19184  oppr1  19315  dfrhm2  19400  rmodislmod  19633  opsrtoslem1  20194  cnfldsub  20503  cnflddiv  20505  dvdsrzring  20560  pjdm  20781  pjfval2  20783  restco  21702  ufprim  22447  tgioo3  23342  oprpiece1res1  23484  oprpiece1res2  23485  volfiniun  24077  vitalilem4  24141  cbvitg  24305  itgresr  24308  cbvditg  24381  plyid  24728  coeidp  24782  dgrid  24783  sincos3rdpi  25031  logblog  25297  ang180lem2  25315  1cubrlem  25346  asin1  25399  log2ublem2  25453  log2ublem3  25454  emcllem5  25505  lgsdir2lem5  25833  lgsquadlem3  25886  2lgslem1b  25896  2lgsoddprmlem3d  25917  cchhllem  26601  ax5seglem7  26649  vtxval0  26752  iedgval0  26753  finsumvtxdg2ssteplem1  27255  wwlksnfi  27612  1wlkdlem1  27844  ex-un  28131  ex-pw  28136  ex-cnv  28144  ex-co  28145  bafval  28309  vsfval  28338  cnnvba  28384  cnnvm  28387  ip2dii  28549  siilem1  28556  h2hcau  28684  hvsubsub4i  28764  hvnegdii  28767  normlem3  28817  normlem8  28822  norm-iii-i  28844  normpar2i  28861  polid2i  28862  chjassi  29191  chj4i  29228  h1de2i  29258  spanunsni  29284  fh3i  29328  fh4i  29329  qlax4i  29335  qlaxr3i  29341  3oalem5  29371  pjadjii  29379  pjsubii  29383  hoadd32i  29483  cnvadj  29597  hh0oi  29608  hhcno  29609  hhcnf  29610  nmopnegi  29670  lnophmlem2  29722  branmfn  29810  dmrab  30188  abrexexd  30197  cbviunf  30236  maprnin  30394  dpmul10  30499  dpexpp1  30512  dpadd3  30516  dpmul  30517  dpmul4  30518  psgnfzto1st  30675  cycpmconjs  30726  lmlimxrge0  31091  zrhre  31160  qqhre  31161  rrhre  31162  cbvesum  31201  unibrsiga  31345  eulerpartlemt  31529  eulerpartgbij  31530  ballotlemrinv  31691  hgt750lem2  31823  bnj1146  31963  bnj893  32100  bnj1234  32183  subfacp1lem1  32324  kur14lem2  32352  kur14lem5  32355  kur14lem7  32357  cvmscld  32418  satfv1lem  32507  fmla0  32527  mvtval  32645  mthmpps  32727  frpoind  32978  frind  32983  frrlem5  33025  noextend  33071  nosupbday  33103  nosupbnd1  33112  nosupbnd2  33114  dmscut  33170  madeval2  33188  fixun  33268  bj-inrab  34143  bj-inrab3  34145  bj-pr1un  34213  bj-pr2un  34227  bj-mpomptALT  34304  rnmptsn  34499  f1omptsnlem  34500  rabiun  34747  phpreu  34758  poimirlem18  34792  ovoliunnfl  34816  voliunnfl  34818  mbfposadd  34821  asindmre  34859  abeqin  35397  rncnvepres  35444  qsresid  35465  rnxrn  35528  xrnres  35532  xrnres2  35533  xrnres3  35534  rncossdmcoss  35577  1cosscnvxrn  35597  refrelsredund4  35749  cdleme25cv  37376  sqdeccom12  39055  nn0expgcd  39064  sn-00idlem2  39109  mendsca  39669  areaquad  39703  cnvrcl0  39865  trclrelexplem  39936  df3o2  40254  df3o3  40255  cbvmpo2  41243  cbvmpo1  41244  mptssid  41391  fprodabs2  41756  stoweidlem13  42179  wallispilem4  42234  fourierdlem94  42366  fourierdlem102  42374  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fourierdlem114  42386  41prothprmlem2  43630  2exp340mod341  43745  8exp8mod9  43748  nfermltl8rev  43754  efmndbas0  43958  cbvmpox2  44282  dmmpossx2  44283  zlmodzxzequa  44449  zlmodzxzequap  44452
  Copyright terms: Public domain W3C validator