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

Theorem 3eqtri 2476
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 2472 . 2  |-  B  =  D
51, 4eqtri 2472 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  csbid  3428  un23  3648  in32  3695  unvdif  3888  undif2  3890  undifabs  3891  difun2  3893  difdifdir  3901  dfif4  3941  dfif5  3942  tpidm23  4118  dfopif  4199  unisn  4249  dfiunv2  4351  unidif0  4610  uniop  4740  suc0  4942  unisuc  4944  iunsuc  4950  xpun  5047  dfrn2  5181  dfdmf  5186  dfrnf  5231  res0  5268  resres  5276  xpssres  5298  dfima2  5329  imai  5339  ima0  5342  imaundir  5409  xpima  5439  dmresv  5455  rescnvcnv  5460  dmtpop  5474  rnsnopg  5477  resdmres  5488  dmmpt  5492  dmco  5505  co01  5512  fresaun  5746  dffv4  5853  fvssunirn  5879  fpr  6064  fvsnun2  6092  mpt20  6352  dmoprab  6368  rnoprab  6370  elrnmpt2res  6401  ov6g  6425  1st0  6791  2nd0  6792  dfmpt2  6875  curry1  6877  curry2  6880  fpar  6889  algrflem  6894  dftpos2  6974  tposoprab  6993  tposmpt2  6994  fvmpt2curryd  7002  tfrlem8  7055  seqomlem3  7119  df2o3  7145  omxpenlem  7620  dfsdom2  7642  marypha2lem2  7898  dfsup2OLD  7905  mapfienOLD  8141  scottexs  8308  scott0s  8309  infxpenc2  8402  infxpenc2OLD  8406  kmlem3  8535  cdaassen  8565  ackbij1lem2  8604  compsscnv  8754  fin1a2lem12  8794  mulerpqlem  9336  1lt2nq  9354  axi2m1  9539  2p2e4  10660  numsuc  10998  numsucc  11012  xnegmnf  11420  pnfaddmnf  11440  fz0tp  11788  fzo0to2pr  11881  fzo0to3tp  11882  fzo0to42pr  11883  i4  12252  binom2aiOLD  12260  crreczi  12273  fac1  12339  fac3  12342  hashkf  12389  hashinf  12392  dmhashres  12396  hashun3  12434  cshwsexa  12774  abs0  13100  absi  13101  trirecip  13656  geoihalfsum  13673  esum  13798  tan0  13868  coshval  13872  ef01bndlem  13901  3dvds  14032  sadc0  14086  gcdmodi  14542  karatsuba  14552  43prm  14589  139prm  14591  631prm  14594  1259lem1  14595  1259lem2  14596  1259lem3  14597  1259lem4  14598  1259lem5  14599  2503lem1  14601  2503lem2  14602  2503lem3  14603  4001lem2  14606  4001lem3  14607  4001lem4  14608  4001prm  14609  ndxarg  14634  xpsc  14936  pmtrsn  16523  psgnprfval1  16526  sylow2a  16618  0frgp  16776  gsumval3OLD  16887  gsumzaddlemOLD  16915  ablfac1eu  17103  sralem  17802  opsrtoslem2  18128  ply1plusgfvi  18262  pf1rcl  18364  restcld  19651  neitr  19659  txbasval  20085  txindis  20113  cnmpt1st  20147  cnmpt2nd  20148  ufildr  20410  restmetu  21068  reust  21791  ismbl  21915  mbfimaopnlem  22040  itg10  22073  itg2cnlem2  22147  itgz  22165  dvmptid  22338  cos2pi  22847  tan4thpi  22885  sincos6thpi  22886  pige3  22888  dfrelog  22931  logm1  22951  dvlog  23010  efopnlem2  23016  cxpexp  23027  root1id  23106  ang180lem2  23120  1cubrlem  23150  quart1  23165  atandm2  23186  efiasin  23197  asinsinlem  23200  asinsin  23201  asin1  23203  acos1  23204  atancj  23219  atanlogsublem  23224  efiatan2  23226  2efiatan  23227  tanatan  23228  dvatan  23244  log2cnv  23253  log2ublem2  23256  log2ublem3  23257  basellem8  23339  ppi1  23416  cht1  23417  chp1  23419  ppi1i  23420  ppi2i  23421  cht2  23424  cht3  23425  bclbnd  23533  bposlem8  23544  ax5seglem7  24216  axlowdimlem8  24230  axlowdimlem11  24233  wlkntrllem2  24540  constr1trl  24568  constr2spthlem1  24574  constr3trllem3  24630  constr3pthlem1  24633  constr3pthlem3  24635  wlknwwlknvbij  24718  clwwlkvbij  24779  vdegp1ai  24962  ex-dif  25122  ex-xp  25135  ex-rn  25139  ip0i  25718  ip1ilem  25719  ipdirilem  25722  ipasslem10  25732  hvnegdii  25957  hvaddcani  25960  hvsubaddi  25961  hisubcomi  25999  normlem0  26004  normlem3  26007  normlem9  26013  bcseqi  26015  norm0  26023  norm-ii-i  26032  norm3difi  26042  normpari  26049  normpar2i  26051  polid2i  26052  shs0i  26345  chj0i  26351  pjsslem  26575  ho0subi  26692  hoaddsubi  26718  hosd1i  26719  hopncani  26721  nmop0  26883  nmfn0  26884  lnopunilem1  26907  lnophmlem2  26914  opsqrlem2  27038  pjclem1  27092  atabsi  27298  dmdbr6ati  27320  inin  27391  iuninc  27406  gtiso  27497  fpwrelmapffs  27535  ordtcnvNEW  27880  ordtrest2NEW  27883  zlmtset  27924  qqhucn  27951  zrhre  27975  qqhre  27976  esumnul  28037  mbfmcst  28208  eulerpartgbij  28289  eulerpartlemn  28298  fib0  28316  fib1  28317  fib2  28319  fib3  28320  fib4  28321  fib5  28322  fib6  28323  0rrv  28368  coinflipprob  28396  ballotlem2  28405  ballotlemfp1  28408  ballotth  28454  signsvf0  28515  derang0  28591  subfac0  28599  subfac1  28600  mthmpps  28920  problem2  28998  quad3  29002  dfrdg2  29204  pred0  29255  trpred0  29295  wfrlem14  29332  wfrlem16  29334  symdif0  29450  symdifid  29452  pprodcnveq  29509  dffv5  29550  fullfunfv  29573  ellines  29778  rankeq1o  29804  onint1  29890  mblfinlem2  30028  ismblfin  30031  dvtan  30041  asindmre  30078  dvasin  30079  dvacos  30080  areacirclem5  30087  heiborlem6  30288  diophrw  30668  dnwech  30970  lmhmlnmsplit  31009  fgraphopab  31146  arearect  31159  areaquad  31160  3lcm2e6  31195  hashnzfz  31201  lhe4.4ex1a  31210  sumnnodd  31590  cosnegpi  31621  itgsin0pilem1  31702  stoweidlem13  31749  wallispilem4  31804  wallispi2lem1  31807  wallispi2lem2  31808  stirlinglem3  31812  dirkertrigeqlem1  31834  fourierdlem56  31899  fourierdlem57  31900  fourierdlem58  31901  fourierdlem62  31905  fourierdlem103  31946  fourierdlem104  31947  fourierdlem112  31955  sqwvfoura  31965  fouriersw  31968  etransclem23  31994  etransclem36  32007  etransclem38  32009  cznrnglem  32588  2t6m3t4e0  32805  zlmodzxzldeplem3  32973  sec0  33024  bnj1416  33963  bj-xpimasn  34395  bj-pr11val  34446  bj-pr21val  34454  bj-pr22val  34460  bj-nuliotaALT  34470  hdmap1cbv  37405  cnvtrrel  37610  xphe  37626
  Copyright terms: Public domain W3C validator