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

Theorem 3eqtri 2460
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 2456 . 2  |-  B  =  D
51, 4eqtri 2456 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  csbid  3258  un23  3506  in32  3553  dfrab2  3616  undifv  3702  undif2  3704  undifabs  3705  difun2  3707  difdifdir  3715  dfif4  3750  dfif5  3751  tpidm23  3907  dfopif  3981  unisn  4031  dfiunv2  4127  unidif0  4372  uniop  4459  suc0  4655  unisuc  4657  iunsuc  4663  xpun  4935  dfrn2  5059  dfdmf  5064  dfrnf  5108  res0  5150  resres  5159  xpssres  5180  dfima2  5205  imai  5218  ima0  5221  imaundir  5285  xpima  5313  dmresv  5329  rescnvcnv  5332  dmtpop  5346  rnsnopg  5349  resdmres  5361  dmmpt  5365  dmco  5378  co01  5384  fresaun  5614  dffv4  5725  fvssunirn  5754  fpr  5914  fvsnun2  5929  dmoprab  6154  rnoprab  6156  ov6g  6211  1st0  6353  2nd0  6354  mpt20  6427  dfmpt2  6437  curry1  6438  curry2  6441  fpar  6450  algrflem  6455  dftpos2  6496  tposoprab  6515  tposmpt2  6516  tfrlem8  6645  seqomlem3  6709  df2o3  6737  omxpenlem  7209  dfsdom2  7230  marypha2lem2  7441  dfsup2OLD  7448  mapfien  7653  scottexs  7811  scott0s  7812  infxpenc2  7903  kmlem3  8032  cdaassen  8062  ackbij1lem2  8101  compsscnv  8251  fin1a2lem12  8291  mulerpqlem  8832  1lt2nq  8850  axi2m1  9034  2p2e4  10098  numsuc  10394  numsucc  10408  xnegmnf  10796  pnfaddmnf  10816  fz0tp  11103  fzo0to2pr  11184  fzo0to3tp  11185  fzo0to42pr  11186  i4  11483  binom2aiOLD  11491  crreczi  11504  fac1  11570  fac3  11573  hashkf  11620  hashinf  11623  hashun3  11658  abs0  12090  absi  12091  trirecip  12642  geoihalfsum  12659  esum  12683  tan0  12752  coshval  12756  ef01bndlem  12785  3dvds  12912  sadc0  12966  gcdmodi  13410  karatsuba  13420  43prm  13444  139prm  13446  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  2503lem1  13456  2503lem2  13457  2503lem3  13458  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  ndxarg  13489  xpsc  13782  sylow2a  15253  0frgp  15411  gsumval3  15514  gsumzaddlem  15526  ablfac1eu  15631  opsrtoslem2  16545  ply1plusgfvi  16636  restcld  17236  neitr  17244  txbasval  17638  txindis  17666  cnmpt1st  17700  cnmpt2nd  17701  ufildr  17963  restmetu  18617  ismbl  19422  mbfimaopnlem  19547  itg10  19580  itg2cnlem2  19654  itgz  19672  dvmptid  19843  pf1rcl  19969  cos2pi  20384  tan4thpi  20422  sincos6thpi  20423  pige3  20425  dfrelog  20463  logm1  20483  dvlog  20542  efopnlem2  20548  cxpexp  20559  root1id  20638  ang180lem2  20652  1cubrlem  20681  quart1  20696  atandm2  20717  efiasin  20728  asinsinlem  20731  asinsin  20732  asin1  20734  acos1  20735  atancj  20750  atanlogsublem  20755  efiatan2  20757  2efiatan  20758  tanatan  20759  dvatan  20775  log2cnv  20784  log2ublem2  20787  log2ublem3  20788  basellem8  20870  ppi1  20947  cht1  20948  chp1  20950  ppi1i  20951  ppi2i  20952  cht2  20955  cht3  20956  bclbnd  21064  bposlem8  21075  wlkntrllem2  21560  constr1trl  21588  constr2spthlem1  21594  constr3trllem3  21639  constr3pthlem1  21642  constr3pthlem3  21644  vdegp1ai  21706  ex-dif  21731  ex-xp  21744  ex-rn  21748  ip0i  22326  ip1ilem  22327  ipdirilem  22330  ipasslem10  22340  hvnegdii  22564  hvaddcani  22567  hvsubaddi  22568  hisubcomi  22606  normlem0  22611  normlem3  22614  normlem9  22620  bcseqi  22622  norm0  22630  norm-ii-i  22639  norm3difi  22649  normpari  22656  normpar2i  22658  polid2i  22659  shs0i  22951  chj0i  22957  pjsslem  23181  ho0subi  23298  hoaddsubi  23324  hosd1i  23325  hopncani  23327  nmop0  23489  nmfn0  23490  lnopunilem1  23513  lnophmlem2  23520  opsqrlem2  23644  pjclem1  23698  atabsi  23904  dmdbr6ati  23926  inin  23996  iuninc  24011  fmptpr  24062  gtiso  24088  dmhashres  24157  reust  24344  zlmtset  24349  qqhucn  24376  rrhcn  24380  zrhre  24385  qqhre  24386  rrhre  24387  esumnul  24443  mbfmcst  24609  0rrv  24709  coinflipprob  24737  ballotlem2  24746  ballotlemfp1  24749  ballotth  24795  derang0  24855  subfac0  24863  subfac1  24864  dfrdg2  25423  pred0  25474  trpred0  25514  wfrlem14  25551  wfrlem16  25553  symdif0  25669  symdifid  25671  pprodcnveq  25728  dffv5  25769  fullfunfv  25792  ax5seglem7  25874  axlowdimlem8  25888  axlowdimlem11  25891  ellines  26086  rankeq1o  26112  onint1  26199  mblfinlem2  26244  ismblfin  26247  dvreasin  26290  areacirclem5  26296  heiborlem6  26525  diophrw  26817  dnwech  27123  lmhmlnmsplit  27162  fgraphopab  27506  lhe4.4ex1a  27523  itgsin0pilem1  27720  stoweidlem13  27738  wallispilem4  27793  wallispi2lem1  27796  wallispi2lem2  27797  stirlinglem3  27801  sec0  28503  bnj1416  29408  hdmap1cbv  32601
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 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator