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

Theorem 3eqtri 2500
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 2496 . 2  |-  B  =  D
51, 4eqtri 2496 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  csbid  3443  un23  3663  in32  3710  unvdif  3901  undif2  3903  undifabs  3904  difun2  3906  difdifdir  3914  dfif4  3954  dfif5  3955  tpidm23  4130  dfopif  4210  unisn  4260  dfiunv2  4361  unidif0  4620  uniop  4750  suc0  4952  unisuc  4954  iunsuc  4960  xpun  5056  dfrn2  5189  dfdmf  5194  dfrnf  5239  res0  5276  resres  5284  xpssres  5306  dfima2  5337  imai  5347  ima0  5350  imaundir  5417  xpima  5447  dmresv  5463  rescnvcnv  5468  dmtpop  5482  rnsnopg  5485  resdmres  5496  dmmpt  5500  dmco  5513  co01  5520  fresaun  5754  dffv4  5861  fvssunirn  5887  fpr  6067  fmptpr  6084  fvsnun2  6095  mpt20  6349  dmoprab  6365  rnoprab  6367  elrnmpt2res  6398  ov6g  6422  1st0  6787  2nd0  6788  dfmpt2  6870  curry1  6872  curry2  6875  fpar  6884  algrflem  6889  dftpos2  6969  tposoprab  6988  tposmpt2  6989  fvmpt2curryd  6997  tfrlem8  7050  seqomlem3  7114  df2o3  7140  omxpenlem  7615  dfsdom2  7637  marypha2lem2  7892  dfsup2OLD  7899  mapfienOLD  8134  scottexs  8301  scott0s  8302  infxpenc2  8395  infxpenc2OLD  8399  kmlem3  8528  cdaassen  8558  ackbij1lem2  8597  compsscnv  8747  fin1a2lem12  8787  mulerpqlem  9329  1lt2nq  9347  axi2m1  9532  2p2e4  10649  numsuc  10984  numsucc  10998  xnegmnf  11405  pnfaddmnf  11425  fz0tp  11771  fzo0to2pr  11863  fzo0to3tp  11864  fzo0to42pr  11865  i4  12234  binom2aiOLD  12242  crreczi  12255  fac1  12321  fac3  12324  hashkf  12371  hashinf  12374  dmhashres  12378  hashun3  12416  cshwsexa  12751  abs0  13077  absi  13078  trirecip  13633  geoihalfsum  13650  esum  13674  tan0  13743  coshval  13747  ef01bndlem  13776  3dvds  13905  sadc0  13959  gcdmodi  14415  karatsuba  14425  43prm  14461  139prm  14463  631prm  14466  1259lem1  14467  1259lem2  14468  1259lem3  14469  1259lem4  14470  1259lem5  14471  2503lem1  14473  2503lem2  14474  2503lem3  14475  4001lem2  14478  4001lem3  14479  4001lem4  14480  4001prm  14481  ndxarg  14506  xpsc  14808  pmtrsn  16340  psgnprfval1  16343  sylow2a  16435  0frgp  16593  gsumval3OLD  16699  gsumzaddlemOLD  16727  ablfac1eu  16914  sralem  17606  opsrtoslem2  17920  ply1plusgfvi  18054  pf1rcl  18156  restcld  19439  neitr  19447  txbasval  19842  txindis  19870  cnmpt1st  19904  cnmpt2nd  19905  ufildr  20167  restmetu  20825  reust  21548  ismbl  21672  mbfimaopnlem  21797  itg10  21830  itg2cnlem2  21904  itgz  21922  dvmptid  22095  cos2pi  22602  tan4thpi  22640  sincos6thpi  22641  pige3  22643  dfrelog  22681  logm1  22701  dvlog  22760  efopnlem2  22766  cxpexp  22777  root1id  22856  ang180lem2  22870  1cubrlem  22900  quart1  22915  atandm2  22936  efiasin  22947  asinsinlem  22950  asinsin  22951  asin1  22953  acos1  22954  atancj  22969  atanlogsublem  22974  efiatan2  22976  2efiatan  22977  tanatan  22978  dvatan  22994  log2cnv  23003  log2ublem2  23006  log2ublem3  23007  basellem8  23089  ppi1  23166  cht1  23167  chp1  23169  ppi1i  23170  ppi2i  23171  cht2  23174  cht3  23175  bclbnd  23283  bposlem8  23294  ax5seglem7  23914  axlowdimlem8  23928  axlowdimlem11  23931  wlkntrllem2  24238  constr1trl  24266  constr2spthlem1  24272  constr3trllem3  24328  constr3pthlem1  24331  constr3pthlem3  24333  wlknwwlknvbij  24416  clwwlkvbij  24477  vdegp1ai  24660  ex-dif  24821  ex-xp  24834  ex-rn  24838  ip0i  25416  ip1ilem  25417  ipdirilem  25420  ipasslem10  25430  hvnegdii  25655  hvaddcani  25658  hvsubaddi  25659  hisubcomi  25697  normlem0  25702  normlem3  25705  normlem9  25711  bcseqi  25713  norm0  25721  norm-ii-i  25730  norm3difi  25740  normpari  25747  normpar2i  25749  polid2i  25750  shs0i  26043  chj0i  26049  pjsslem  26273  ho0subi  26390  hoaddsubi  26416  hosd1i  26417  hopncani  26419  nmop0  26581  nmfn0  26582  lnopunilem1  26605  lnophmlem2  26612  opsqrlem2  26736  pjclem1  26790  atabsi  26996  dmdbr6ati  27018  inin  27087  iuninc  27101  gtiso  27191  fpwrelmapffs  27229  ordtcnvNEW  27538  ordtrest2NEW  27541  zlmtset  27582  qqhucn  27609  rrhcn  27614  zrhre  27633  qqhre  27634  esumnul  27699  mbfmcst  27870  eulerpartgbij  27951  eulerpartlemn  27960  fib0  27978  fib1  27979  fib2  27981  fib3  27982  fib4  27983  fib5  27984  fib6  27985  0rrv  28030  coinflipprob  28058  ballotlem2  28067  ballotlemfp1  28070  ballotth  28116  signsvf0  28177  derang0  28253  subfac0  28261  subfac1  28262  problem2  28495  dfrdg2  28805  pred0  28856  trpred0  28896  wfrlem14  28933  wfrlem16  28935  symdif0  29051  symdifid  29053  pprodcnveq  29110  dffv5  29151  fullfunfv  29174  ellines  29379  rankeq1o  29405  onint1  29491  mblfinlem2  29629  ismblfin  29632  dvtan  29642  asindmre  29679  dvasin  29680  dvacos  29681  areacirclem5  29688  heiborlem6  29915  diophrw  30296  dnwech  30598  lmhmlnmsplit  30637  fgraphopab  30775  arearect  30788  areaquad  30789  3lcm2e6  30819  hashnzfz  30825  lhe4.4ex1a  30834  sumnnodd  31172  cosnegpi  31203  itgsin0pilem1  31267  stoweidlem13  31313  wallispilem4  31368  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem3  31376  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem3  31400  dirkercncflem1  31403  fourierdlem56  31463  fourierdlem57  31464  fourierdlem58  31465  fourierdlem62  31469  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem112  31519  fourierdlem113  31520  sqwvfoura  31529  fourierswlem  31531  fouriersw  31532  2t6m3t4e0  32001  zlmodzxzldeplem3  32184  sec0  32235  bnj1416  33174  bj-xpimasn  33593  bj-pr11val  33644  bj-pr21val  33652  bj-pr22val  33658  bj-nuliotaALT  33668  hdmap1cbv  36600  cnvtrrel  36792
  Copyright terms: Public domain W3C validator