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

Theorem 3eqtri 2488
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 2484 . 2  |-  B  =  D
51, 4eqtri 2484 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455
This theorem is referenced by:  csbid  3383  un23  3605  in32  3656  unvdif  3853  undif2  3855  undifabs  3856  difun2  3859  difdifdir  3867  dfif4  3908  dfif5  3909  tpidm23  4088  dfopif  4177  unisn  4227  dfiunv2  4328  symdif0  4369  symdifid  4371  unidif0  4590  uniop  4718  xpun  4911  dfrn2  5042  dfdmf  5047  dfrnf  5092  res0  5128  resres  5136  xpssres  5158  dfima2  5189  imai  5199  ima0  5202  imaundir  5268  xpima  5298  dmresv  5313  rescnvcnv  5317  dmtpop  5331  rnsnopg  5334  resdmres  5345  dmmpt  5349  dmco  5362  co01  5369  pred0  5429  suc0  5516  unisuc  5518  iunsuc  5524  fresaun  5777  dffv4  5885  fvssunirn  5911  fpr  6096  fvsnun2  6124  mpt20  6388  dmoprab  6404  rnoprab  6406  elrnmpt2res  6437  ov6g  6461  1st0  6826  2nd0  6827  dfmpt2  6913  curry1  6915  curry2  6918  fpar  6927  algrflem  6932  dftpos2  7016  tposoprab  7035  tposmpt2  7036  fvmpt2curryd  7044  wfrlem14  7075  wfrlem16  7077  dfrecs3  7117  tfrlem8  7128  seqomlem3  7195  df2o3  7221  omxpenlem  7699  dfsdom2  7721  marypha2lem2  7976  scottexs  8384  scott0s  8385  infxpenc2  8479  kmlem3  8608  cdaassen  8638  ackbij1lem2  8677  compsscnv  8827  fin1a2lem12  8867  mulerpqlem  9406  1lt2nq  9424  axi2m1  9609  2p2e4  10756  numsuc  11092  numsucc  11106  xnegmnf  11532  pnfaddmnf  11552  fz0tp  11922  fz0to3un2pr  11923  fzo13pr  12028  fzo0to2pr  12029  fzo0to3tp  12030  fzo0to42pr  12031  i4  12409  crreczi  12429  fac1  12495  fac3  12498  hashkf  12549  hashinf  12552  dmhashres  12556  hashun3  12595  cshwsexa  12960  dmtrclfv  13131  abs0  13397  absi  13398  trirecip  13970  geoihalfsum  13987  esum  14184  tan0  14254  coshval  14258  ef01bndlem  14287  3dvds  14418  sadc0  14477  3lcm2e6woprm  14629  6lcm4e12  14630  lcmf0  14656  prmo0  15043  gcdmodi  15095  karatsuba  15105  43prm  15142  139prm  15144  631prm  15147  1259lem1  15151  1259lem2  15152  1259lem3  15153  1259lem4  15154  1259lem5  15155  2503lem1  15157  2503lem2  15158  2503lem3  15159  4001lem2  15162  4001lem3  15163  4001lem4  15164  4001prm  15165  ndxarg  15190  xpsc  15512  pmtrsn  17209  psgnprfval1  17212  sylow2a  17320  0frgp  17478  ablfac1eu  17755  sralem  18449  opsrtoslem2  18757  ply1plusgfvi  18884  pf1rcl  18986  restcld  20237  neitr  20245  txbasval  20670  txindis  20698  cnmpt1st  20732  cnmpt2nd  20733  ufildr  20995  restmetu  21634  reust  22389  ismbl  22529  mbfimaopnlem  22660  itg10  22695  itg2cnlem2  22769  itgz  22787  dvmptid  22960  cos2pi  23480  tan4thpi  23518  sincos6thpi  23519  pige3  23521  dfrelog  23564  logm1  23587  dvlog  23645  efopnlem2  23651  cxpexp  23662  root1id  23743  ang180lem2  23788  1cubrlem  23816  quart1  23831  atandm2  23852  efiasin  23863  asinsinlem  23866  asinsin  23867  asin1  23869  acos1  23870  atancj  23885  atanlogsublem  23890  efiatan2  23892  2efiatan  23893  tanatan  23894  dvatan  23910  log2cnv  23919  log2ublem2  23922  log2ublem3  23923  basellem8  24063  ppi1  24140  cht1  24141  chp1  24143  ppi1i  24144  ppi2i  24145  cht2  24148  cht3  24149  bclbnd  24257  bposlem8  24268  ax5seglem7  25014  axlowdimlem8  25028  axlowdimlem11  25031  wlkntrllem2  25339  constr1trl  25367  constr2spthlem1  25373  constr3trllem3  25429  constr3pthlem1  25432  constr3pthlem3  25434  wlknwwlknvbij  25517  clwwlkvbij  25578  vdegp1ai  25761  ex-dif  25922  ex-xp  25935  ex-rn  25939  ip0i  26515  ip1ilem  26516  ipdirilem  26519  ipasslem10  26529  hvnegdii  26764  hvaddcani  26767  hvsubaddi  26768  hisubcomi  26806  normlem0  26811  normlem3  26814  normlem9  26820  bcseqi  26822  norm0  26830  norm-ii-i  26839  norm3difi  26849  normpari  26856  normpar2i  26858  polid2i  26859  shs0i  27151  chj0i  27157  pjsslem  27381  ho0subi  27497  hoaddsubi  27523  hosd1i  27524  hopncani  27526  nmop0  27688  nmfn0  27689  lnopunilem1  27712  lnophmlem2  27719  opsqrlem2  27843  pjclem1  27897  atabsi  28103  dmdbr6ati  28125  inin  28198  iuninc  28225  gtiso  28330  fpwrelmapffs  28368  lmat22det  28697  ordtcnvNEW  28775  ordtrest2NEW  28778  zlmtset  28818  qqhucn  28845  zrhre  28872  qqhre  28873  esumnul  28918  mbfmcst  29130  carsggect  29199  eulerpartgbij  29254  eulerpartlemn  29263  fib0  29281  fib1  29282  fib2  29284  fib3  29285  fib4  29286  fib5  29287  fib6  29288  0rrv  29333  coinflipprob  29361  ballotlem2  29370  ballotlemfp1  29373  ballotth  29419  ballotthOLD  29457  signsvf0  29518  bnj1416  29897  derang0  29941  subfac0  29949  subfac1  29950  mthmpps  30269  problem2  30347  quad3  30351  dfrdg2  30491  trpred0  30526  pprodcnveq  30699  dffv5  30740  fullfunfv  30763  ellines  30968  rankeq1o  30987  onint1  31158  bj-xpimasn  31593  bj-pr11val  31644  bj-pr21val  31652  bj-pr22val  31658  bj-nuliotaALT  31669  bj-dfmpt2a  31675  icorempt2  31799  finxpreclem4  31831  finxp2o  31836  finxp3o  31837  poimirlem5  31990  poimirlem22  32007  poimirlem26  32011  poimirlem30  32015  mblfinlem2  32023  ismblfin  32026  dvtan  32037  asindmre  32072  dvasin  32073  dvacos  32074  areacirclem5  32081  heiborlem6  32193  hdmap1cbv  35416  diophrw  35646  dnwech  35951  lmhmlnmsplit  35990  fgraphopab  36132  arearect  36145  areaquad  36146  dmnonrel  36241  imanonrel  36244  cononrel1  36245  cononrel2  36246  rclexi  36267  dfrtrcl5  36281  cnvtrrel  36307  dfrcl2  36311  dfrcl4  36313  iunrelexp0  36339  comptiunov2i  36343  relexpaddss  36355  brtrclfv2  36364  trclfvdecomr  36365  corcltrcl  36376  cotrclrcl  36379  xpheOLD  36422  hashnzfz  36713  lhe4.4ex1a  36722  disjinfi  37506  sumnnodd  37748  cosnegpi  37780  itgsin0pilem1  37864  stoweidlem13  37911  wallispilem4  37968  wallispi2lem1  37971  wallispi2lem2  37972  stirlinglem3  37976  dirkertrigeqlem1  37998  fourierdlem56  38064  fourierdlem57  38065  fourierdlem58  38066  fourierdlem62  38070  fourierdlem103  38111  fourierdlem104  38112  fourierdlem112  38120  sqwvfoura  38130  fouriersw  38133  etransclem23  38160  etransclem36  38173  etransclem38  38175  carageniuncllem1  38380  0ome  38388  ovn02  38428  nnsum3primesgbe  38925  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  bgoldbtbndlem1  38938  tgoldbachlt  38947  5tcu2e40  38953  3exp4mod41  38954  41prothprmlem2  38956  41prothprm  38957  usgrexmpledg  39384  umgrislfupgrlem  39718  uhgr1wlkspthlem2  39786  1wlk2v2elem2  39871  cznrnglem  40228  2t6m3t4e0  40402  zlmodzxzldeplem3  40568  sec0  40753
  Copyright terms: Public domain W3C validator