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

Theorem 3eqtri 2454
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 2450 . 2  |-  B  =  D
51, 4eqtri 2450 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  csbid  3245  un23  3493  in32  3540  dfrab2  3603  undifv  3689  undif2  3691  undifabs  3692  difun2  3694  difdifdir  3702  dfif4  3737  dfif5  3738  tpidm23  3894  dfopif  3968  unisn  4018  dfiunv2  4114  unidif0  4359  uniop  4446  suc0  4642  unisuc  4644  iunsuc  4650  xpun  4921  dfrn2  5045  dfdmf  5050  dfrnf  5094  res0  5136  resres  5145  xpssres  5166  dfima2  5191  imai  5204  ima0  5207  imaundir  5271  xpima  5299  dmresv  5315  rescnvcnv  5318  dmtpop  5332  rnsnopg  5335  resdmres  5347  dmmpt  5351  dmco  5364  co01  5370  fresaun  5600  dffv4  5711  fvssunirn  5740  fpr  5900  fvsnun2  5915  dmoprab  6140  rnoprab  6142  ov6g  6197  1st0  6339  2nd0  6340  mpt20  6413  dfmpt2  6423  curry1  6424  curry2  6427  fpar  6436  algrflem  6441  dftpos2  6482  tposoprab  6501  tposmpt2  6502  tfrlem8  6631  seqomlem3  6695  df2o3  6723  omxpenlem  7195  dfsdom2  7216  marypha2lem2  7427  dfsup2OLD  7434  mapfien  7637  scottexs  7795  scott0s  7796  infxpenc2  7887  kmlem3  8016  cdaassen  8046  ackbij1lem2  8085  compsscnv  8235  fin1a2lem12  8275  mulerpqlem  8816  1lt2nq  8834  axi2m1  9018  2p2e4  10082  numsuc  10378  numsucc  10392  xnegmnf  10780  pnfaddmnf  10800  fz0tp  11087  fzo0to2pr  11167  fzo0to3tp  11168  fzo0to42pr  11169  i4  11466  binom2aiOLD  11474  crreczi  11487  fac1  11553  fac3  11556  hashkf  11603  hashinf  11606  hashun3  11641  abs0  12073  absi  12074  trirecip  12625  geoihalfsum  12642  esum  12666  tan0  12735  coshval  12739  ef01bndlem  12768  3dvds  12895  sadc0  12949  gcdmodi  13393  karatsuba  13403  43prm  13427  139prm  13429  631prm  13432  1259lem1  13433  1259lem2  13434  1259lem3  13435  1259lem4  13436  1259lem5  13437  2503lem1  13439  2503lem2  13440  2503lem3  13441  4001lem2  13444  4001lem3  13445  4001lem4  13446  4001prm  13447  ndxarg  13472  xpsc  13765  sylow2a  15236  0frgp  15394  gsumval3  15497  gsumzaddlem  15509  ablfac1eu  15614  opsrtoslem2  16528  ply1plusgfvi  16619  restcld  17219  neitr  17227  txbasval  17621  txindis  17649  cnmpt1st  17683  cnmpt2nd  17684  ufildr  17946  restmetu  18600  ismbl  19405  mbfimaopnlem  19530  itg10  19563  itg2cnlem2  19637  itgz  19655  dvmptid  19826  pf1rcl  19952  cos2pi  20367  tan4thpi  20405  sincos6thpi  20406  pige3  20408  dfrelog  20446  logm1  20466  dvlog  20525  efopnlem2  20531  cxpexp  20542  root1id  20621  ang180lem2  20635  1cubrlem  20664  quart1  20679  atandm2  20700  efiasin  20711  asinsinlem  20714  asinsin  20715  asin1  20717  acos1  20718  atancj  20733  atanlogsublem  20738  efiatan2  20740  2efiatan  20741  tanatan  20742  dvatan  20758  log2cnv  20767  log2ublem2  20770  log2ublem3  20771  basellem8  20853  ppi1  20930  cht1  20931  chp1  20933  ppi1i  20934  ppi2i  20935  cht2  20938  cht3  20939  bclbnd  21047  bposlem8  21058  wlkntrllem2  21543  constr1trl  21571  constr2spthlem1  21577  constr3trllem3  21622  constr3pthlem1  21625  constr3pthlem3  21627  vdegp1ai  21689  ex-dif  21714  ex-xp  21727  ex-rn  21731  ip0i  22309  ip1ilem  22310  ipdirilem  22313  ipasslem10  22323  hvnegdii  22547  hvaddcani  22550  hvsubaddi  22551  hisubcomi  22589  normlem0  22594  normlem3  22597  normlem9  22603  bcseqi  22605  norm0  22613  norm-ii-i  22622  norm3difi  22632  normpari  22639  normpar2i  22641  polid2i  22642  shs0i  22934  chj0i  22940  pjsslem  23164  ho0subi  23281  hoaddsubi  23307  hosd1i  23308  hopncani  23310  nmop0  23472  nmfn0  23473  lnopunilem1  23496  lnophmlem2  23503  opsqrlem2  23627  pjclem1  23681  atabsi  23887  dmdbr6ati  23909  inin  23979  iuninc  23994  fmptpr  24045  gtiso  24071  dmhashres  24140  reust  24327  zlmtset  24332  qqhucn  24359  rrhcn  24363  zrhre  24368  qqhre  24369  rrhre  24370  esumnul  24426  mbfmcst  24592  0rrv  24692  coinflipprob  24720  ballotlem2  24729  ballotlemfp1  24732  ballotth  24778  derang0  24838  subfac0  24846  subfac1  24847  dfrdg2  25402  pred0  25449  trpred0  25489  wfrlem14  25519  wfrlem16  25521  symdif0  25618  symdifid  25620  pprodcnveq  25673  dffv5  25714  fullfunfv  25737  ax5seglem7  25817  axlowdimlem8  25831  axlowdimlem11  25834  ellines  26029  rankeq1o  26055  onint1  26142  mblfinlem  26185  ismblfin  26188  dvreasin  26221  areacirclem6  26228  heiborlem6  26457  diophrw  26749  dnwech  27055  lmhmlnmsplit  27095  fgraphopab  27439  lhe4.4ex1a  27456  itgsin0pilem1  27653  stoweidlem13  27671  wallispilem4  27726  wallispi2lem1  27729  wallispi2lem2  27730  stirlinglem3  27734  sec0  28259  bnj1416  29160  hdmap1cbv  32332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2423
  Copyright terms: Public domain W3C validator