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

Theorem 3eqtri 2467
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 2463 . 2  |-  B  =  D
51, 4eqtri 2463 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  csbid  3311  un23  3530  in32  3577  unvdif  3768  undif2  3770  undifabs  3771  difun2  3773  difdifdir  3781  dfif4  3819  dfif5  3820  tpidm23  3993  dfopif  4071  unisn  4121  dfiunv2  4221  unidif0  4480  uniop  4609  suc0  4808  unisuc  4810  iunsuc  4816  xpun  4911  dfrn2  5043  dfdmf  5048  dfrnf  5093  res0  5130  resres  5138  xpssres  5159  dfima2  5186  imai  5196  ima0  5199  imaundir  5265  xpima  5295  dmresv  5311  rescnvcnv  5316  dmtpop  5330  rnsnopg  5333  resdmres  5344  dmmpt  5348  dmco  5361  co01  5367  fresaun  5597  dffv4  5703  fvssunirn  5728  fpr  5905  fmptpr  5918  fvsnun2  5929  mpt20  6171  dmoprab  6186  rnoprab  6188  elrnmpt2res  6219  ov6g  6243  1st0  6598  2nd0  6599  dfmpt2  6678  curry1  6679  curry2  6682  fpar  6691  algrflem  6696  dftpos2  6777  tposoprab  6796  tposmpt2  6797  fvmpt2curryd  6805  tfrlem8  6858  seqomlem3  6922  df2o3  6948  omxpenlem  7427  dfsdom2  7449  marypha2lem2  7701  dfsup2OLD  7708  mapfienOLD  7942  scottexs  8109  scott0s  8110  infxpenc2  8203  infxpenc2OLD  8207  kmlem3  8336  cdaassen  8366  ackbij1lem2  8405  compsscnv  8555  fin1a2lem12  8595  mulerpqlem  9139  1lt2nq  9157  axi2m1  9341  2p2e4  10454  numsuc  10782  numsucc  10796  xnegmnf  11195  pnfaddmnf  11215  fz0tp  11528  fzo0to2pr  11629  fzo0to3tp  11630  fzo0to42pr  11631  i4  11983  binom2aiOLD  11991  crreczi  12004  fac1  12070  fac3  12073  hashkf  12120  hashinf  12123  dmhashres  12127  hashun3  12162  cshwsexa  12473  abs0  12789  absi  12790  trirecip  13340  geoihalfsum  13357  esum  13381  tan0  13450  coshval  13454  ef01bndlem  13483  3dvds  13611  sadc0  13665  gcdmodi  14118  karatsuba  14128  43prm  14164  139prm  14166  631prm  14169  1259lem1  14170  1259lem2  14171  1259lem3  14172  1259lem4  14173  1259lem5  14174  2503lem1  14176  2503lem2  14177  2503lem3  14178  4001lem2  14181  4001lem3  14182  4001lem4  14183  4001prm  14184  ndxarg  14209  xpsc  14510  psgnprfval1  16041  sylow2a  16133  0frgp  16291  gsumval3OLD  16397  gsumzaddlemOLD  16425  ablfac1eu  16589  sralem  17273  opsrtoslem2  17581  ply1plusgfvi  17712  pf1rcl  17798  restcld  18791  neitr  18799  txbasval  19194  txindis  19222  cnmpt1st  19256  cnmpt2nd  19257  ufildr  19519  restmetu  20177  reust  20900  ismbl  21024  mbfimaopnlem  21148  itg10  21181  itg2cnlem2  21255  itgz  21273  dvmptid  21446  cos2pi  21953  tan4thpi  21991  sincos6thpi  21992  pige3  21994  dfrelog  22032  logm1  22052  dvlog  22111  efopnlem2  22117  cxpexp  22128  root1id  22207  ang180lem2  22221  1cubrlem  22251  quart1  22266  atandm2  22287  efiasin  22298  asinsinlem  22301  asinsin  22302  asin1  22304  acos1  22305  atancj  22320  atanlogsublem  22325  efiatan2  22327  2efiatan  22328  tanatan  22329  dvatan  22345  log2cnv  22354  log2ublem2  22357  log2ublem3  22358  basellem8  22440  ppi1  22517  cht1  22518  chp1  22520  ppi1i  22521  ppi2i  22522  cht2  22525  cht3  22526  bclbnd  22634  bposlem8  22645  ax5seglem7  23196  axlowdimlem8  23210  axlowdimlem11  23213  wlkntrllem2  23474  constr1trl  23502  constr2spthlem1  23508  constr3trllem3  23553  constr3pthlem1  23556  constr3pthlem3  23558  vdegp1ai  23620  ex-dif  23645  ex-xp  23658  ex-rn  23662  ip0i  24240  ip1ilem  24241  ipdirilem  24244  ipasslem10  24254  hvnegdii  24479  hvaddcani  24482  hvsubaddi  24483  hisubcomi  24521  normlem0  24526  normlem3  24529  normlem9  24535  bcseqi  24537  norm0  24545  norm-ii-i  24554  norm3difi  24564  normpari  24571  normpar2i  24573  polid2i  24574  shs0i  24867  chj0i  24873  pjsslem  25097  ho0subi  25214  hoaddsubi  25240  hosd1i  25241  hopncani  25243  nmop0  25405  nmfn0  25406  lnopunilem1  25429  lnophmlem2  25436  opsqrlem2  25560  pjclem1  25614  atabsi  25820  dmdbr6ati  25842  inin  25911  iuninc  25926  gtiso  26011  fpwrelmapffs  26049  ordtcnvNEW  26365  ordtrest2NEW  26368  zlmtset  26409  qqhucn  26436  rrhcn  26441  zrhre  26460  qqhre  26461  esumnul  26517  mbfmcst  26689  eulerpartgbij  26770  eulerpartlemn  26779  fib0  26797  fib1  26798  fib2  26800  fib3  26801  fib4  26802  fib5  26803  fib6  26804  0rrv  26849  coinflipprob  26877  ballotlem2  26886  ballotlemfp1  26889  ballotth  26935  signsvf0  26996  derang0  27072  subfac0  27080  subfac1  27081  problem2  27314  dfrdg2  27624  pred0  27675  trpred0  27715  wfrlem14  27752  wfrlem16  27754  symdif0  27870  symdifid  27872  pprodcnveq  27929  dffv5  27970  fullfunfv  27993  ellines  28198  rankeq1o  28224  onint1  28310  mblfinlem2  28448  ismblfin  28451  dvtan  28461  asindmre  28498  dvasin  28499  dvacos  28500  areacirclem5  28507  heiborlem6  28734  diophrw  29116  dnwech  29420  lmhmlnmsplit  29459  fgraphopab  29597  arearect  29610  areaquad  29611  lhe4.4ex1a  29622  itgsin0pilem1  29809  stoweidlem13  29827  wallispilem4  29882  wallispi2lem1  29885  wallispi2lem2  29886  stirlinglem3  29890  wlknwwlknvbij  30391  clwwlkvbij  30482  2t6m3t4e0  30759  pmtrsn  30789  pmatcollpw1dst  30920  mp2pm2mplem3  30937  pmattomply1fo  30942  pmattomply1mhmlem2  30948  zlmodzxzldeplem3  31063  sec0  31114  bnj1416  32049  bj-xpimasn  32466  bj-pr11val  32517  bj-pr21val  32525  bj-pr22val  32531  hdmap1cbv  35467
  Copyright terms: Public domain W3C validator