MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtri Structured version   Unicode version

Theorem 3eqtri 2465
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
Hypotheses
Ref Expression
3eqtri.1  |-  A  =  B
3eqtri.2  |-  B  =  C
3eqtri.3  |-  C  =  D
Assertion
Ref Expression
3eqtri  |-  A  =  D

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2  |-  A  =  B
2 3eqtri.2 . . 3  |-  B  =  C
3 3eqtri.3 . . 3  |-  C  =  D
42, 3eqtri 2461 . 2  |-  B  =  D
51, 4eqtri 2461 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434
This theorem is referenced by:  csbid  3293  un23  3512  in32  3559  unvdif  3750  undif2  3752  undifabs  3753  difun2  3755  difdifdir  3763  dfif4  3801  dfif5  3802  tpidm23  3975  dfopif  4053  unisn  4103  dfiunv2  4203  unidif0  4462  uniop  4591  suc0  4789  unisuc  4791  iunsuc  4797  xpun  4892  dfrn2  5024  dfdmf  5029  dfrnf  5074  res0  5111  resres  5120  xpssres  5141  dfima2  5168  imai  5178  ima0  5181  imaundir  5247  xpima  5277  dmresv  5293  rescnvcnv  5298  dmtpop  5312  rnsnopg  5315  resdmres  5326  dmmpt  5330  dmco  5343  co01  5349  fresaun  5579  dffv4  5685  fvssunirn  5710  fpr  5887  fmptpr  5900  fvsnun2  5911  mpt20  6155  dmoprab  6170  rnoprab  6172  elrnmpt2res  6203  ov6g  6227  1st0  6582  2nd0  6583  dfmpt2  6662  curry1  6663  curry2  6666  fpar  6675  algrflem  6680  dftpos2  6761  tposoprab  6780  tposmpt2  6781  tfrlem8  6839  seqomlem3  6903  df2o3  6929  omxpenlem  7408  dfsdom2  7430  marypha2lem2  7682  dfsup2OLD  7689  mapfienOLD  7923  scottexs  8090  scott0s  8091  infxpenc2  8184  infxpenc2OLD  8188  kmlem3  8317  cdaassen  8347  ackbij1lem2  8386  compsscnv  8536  fin1a2lem12  8576  mulerpqlem  9120  1lt2nq  9138  axi2m1  9322  2p2e4  10435  numsuc  10763  numsucc  10777  xnegmnf  11176  pnfaddmnf  11196  fz0tp  11509  fzo0to2pr  11610  fzo0to3tp  11611  fzo0to42pr  11612  i4  11964  binom2aiOLD  11972  crreczi  11985  fac1  12051  fac3  12054  hashkf  12101  hashinf  12104  dmhashres  12108  hashun3  12143  cshwsexa  12454  abs0  12770  absi  12771  trirecip  13321  geoihalfsum  13338  esum  13362  tan0  13431  coshval  13435  ef01bndlem  13464  3dvds  13592  sadc0  13646  gcdmodi  14099  karatsuba  14109  43prm  14145  139prm  14147  631prm  14150  1259lem1  14151  1259lem2  14152  1259lem3  14153  1259lem4  14154  1259lem5  14155  2503lem1  14157  2503lem2  14158  2503lem3  14159  4001lem2  14162  4001lem3  14163  4001lem4  14164  4001prm  14165  ndxarg  14190  xpsc  14491  psgnprfval1  16019  sylow2a  16111  0frgp  16269  gsumval3OLD  16375  gsumzaddlemOLD  16403  ablfac1eu  16564  sralem  17236  opsrtoslem2  17542  ply1plusgfvi  17672  pf1rcl  17752  restcld  18735  neitr  18743  txbasval  19138  txindis  19166  cnmpt1st  19200  cnmpt2nd  19201  ufildr  19463  restmetu  20121  reust  20844  ismbl  20968  mbfimaopnlem  21092  itg10  21125  itg2cnlem2  21199  itgz  21217  dvmptid  21390  cos2pi  21897  tan4thpi  21935  sincos6thpi  21936  pige3  21938  dfrelog  21976  logm1  21996  dvlog  22055  efopnlem2  22061  cxpexp  22072  root1id  22151  ang180lem2  22165  1cubrlem  22195  quart1  22210  atandm2  22231  efiasin  22242  asinsinlem  22245  asinsin  22246  asin1  22248  acos1  22249  atancj  22264  atanlogsublem  22269  efiatan2  22271  2efiatan  22272  tanatan  22273  dvatan  22289  log2cnv  22298  log2ublem2  22301  log2ublem3  22302  basellem8  22384  ppi1  22461  cht1  22462  chp1  22464  ppi1i  22465  ppi2i  22466  cht2  22469  cht3  22470  bclbnd  22578  bposlem8  22589  ax5seglem7  23116  axlowdimlem8  23130  axlowdimlem11  23133  wlkntrllem2  23394  constr1trl  23422  constr2spthlem1  23428  constr3trllem3  23473  constr3pthlem1  23476  constr3pthlem3  23478  vdegp1ai  23540  ex-dif  23565  ex-xp  23578  ex-rn  23582  ip0i  24160  ip1ilem  24161  ipdirilem  24164  ipasslem10  24174  hvnegdii  24399  hvaddcani  24402  hvsubaddi  24403  hisubcomi  24441  normlem0  24446  normlem3  24449  normlem9  24455  bcseqi  24457  norm0  24465  norm-ii-i  24474  norm3difi  24484  normpari  24491  normpar2i  24493  polid2i  24494  shs0i  24787  chj0i  24793  pjsslem  25017  ho0subi  25134  hoaddsubi  25160  hosd1i  25161  hopncani  25163  nmop0  25325  nmfn0  25326  lnopunilem1  25349  lnophmlem2  25356  opsqrlem2  25480  pjclem1  25534  atabsi  25740  dmdbr6ati  25762  inin  25831  iuninc  25846  gtiso  25931  fpwrelmapffs  25969  ordtcnvNEW  26286  ordtrest2NEW  26289  zlmtset  26330  qqhucn  26357  rrhcn  26362  zrhre  26381  qqhre  26382  esumnul  26438  mbfmcst  26610  eulerpartgbij  26685  eulerpartlemn  26694  fib0  26712  fib1  26713  fib2  26715  fib3  26716  fib4  26717  fib5  26718  fib6  26719  0rrv  26764  coinflipprob  26792  ballotlem2  26801  ballotlemfp1  26804  ballotth  26850  signsvf0  26911  derang0  26987  subfac0  26995  subfac1  26996  problem2  27229  dfrdg2  27538  pred0  27589  trpred0  27629  wfrlem14  27666  wfrlem16  27668  symdif0  27784  symdifid  27786  pprodcnveq  27843  dffv5  27884  fullfunfv  27907  ellines  28112  rankeq1o  28138  onint1  28225  mblfinlem2  28354  ismblfin  28357  dvtan  28367  asindmre  28404  dvasin  28405  dvacos  28406  areacirclem5  28413  heiborlem6  28640  diophrw  29022  dnwech  29326  lmhmlnmsplit  29365  fgraphopab  29503  arearect  29516  lhe4.4ex1a  29528  itgsin0pilem1  29715  stoweidlem13  29733  wallispilem4  29788  wallispi2lem1  29791  wallispi2lem2  29792  stirlinglem3  29796  wlknwwlknvbij  30297  clwwlkvbij  30388  2t6m3t4e0  30664  pmtrsn  30687  zlmodzxzldeplem3  30885  sec0  30936  bnj1416  31864  bj-xpimasn  32177  bj-pr11val  32228  bj-pr21val  32236  bj-pr22val  32242  hdmap1cbv  35170
  Copyright terms: Public domain W3C validator