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

Theorem 3eqtri 2404
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 2400 . 2  |-  B  =  D
51, 4eqtri 2400 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  csbid  3194  un23  3442  in32  3489  dfrab2  3552  undifv  3638  undif2  3640  undifabs  3641  difun2  3643  difdifdir  3651  dfif4  3686  dfif5  3687  tpidm23  3843  dfopif  3916  unisn  3966  unidif0  4306  uniop  4393  suc0  4589  unisuc  4591  iunsuc  4597  xpun  4868  dfrn2  4992  dfdmf  4997  dfrnf  5041  res0  5083  resres  5092  xpssres  5113  dfima2  5138  imai  5151  ima0  5154  imaundir  5218  xpima  5246  dmresv  5262  rescnvcnv  5265  dmtpop  5279  rnsnopg  5282  resdmres  5294  dmmpt  5298  dmco  5311  co01  5317  fresaun  5547  dffv4  5658  fvssunirn  5687  fpr  5846  fvsnun2  5861  dmoprab  6086  rnoprab  6088  ov6g  6143  1st0  6285  2nd0  6286  mpt20  6359  dfmpt2  6369  curry1  6370  curry2  6373  fpar  6382  algrflem  6384  dftpos2  6425  tposoprab  6444  tposmpt2  6445  tfrlem8  6574  seqomlem3  6638  df2o3  6666  omxpenlem  7138  dfsdom2  7159  marypha2lem2  7369  dfsup2OLD  7376  mapfien  7579  scottexs  7737  scott0s  7738  infxpenc2  7829  kmlem3  7958  cdaassen  7988  ackbij1lem2  8027  compsscnv  8177  fin1a2lem12  8217  mulerpqlem  8758  1lt2nq  8776  axi2m1  8960  2p2e4  10023  numsuc  10319  numsucc  10333  xnegmnf  10721  pnfaddmnf  10741  fzo0to2pr  11104  fzo0to3tp  11105  fzo0to42pr  11106  i4  11403  binom2aiOLD  11411  crreczi  11424  fac1  11490  fac3  11493  hashkf  11540  hashinf  11543  hashun3  11578  abs0  12010  absi  12011  trirecip  12562  geoihalfsum  12579  esum  12603  tan0  12672  coshval  12676  ef01bndlem  12705  3dvds  12832  sadc0  12886  gcdmodi  13330  karatsuba  13340  43prm  13364  139prm  13366  631prm  13369  1259lem1  13370  1259lem2  13371  1259lem3  13372  1259lem4  13373  1259lem5  13374  2503lem1  13376  2503lem2  13377  2503lem3  13378  4001lem2  13381  4001lem3  13382  4001lem4  13383  4001prm  13384  ndxarg  13409  xpsc  13702  sylow2a  15173  0frgp  15331  gsumval3  15434  gsumzaddlem  15446  ablfac1eu  15551  opsrtoslem2  16465  ply1plusgfvi  16556  restcld  17151  neitr  17159  txbasval  17552  txindis  17580  cnmpt1st  17614  cnmpt2nd  17615  ufildr  17877  restmetu  18482  ismbl  19282  mbfimaopnlem  19407  itg10  19440  itg2cnlem2  19514  itgz  19532  dvmptid  19703  pf1rcl  19829  cos2pi  20244  tan4thpi  20282  sincos6thpi  20283  pige3  20285  dfrelog  20323  logm1  20343  dvlog  20402  efopnlem2  20408  cxpexp  20419  root1id  20498  ang180lem2  20512  1cubrlem  20541  quart1  20556  atandm2  20577  efiasin  20588  asinsinlem  20591  asinsin  20592  asin1  20594  acos1  20595  atancj  20610  atanlogsublem  20615  efiatan2  20617  2efiatan  20618  tanatan  20619  dvatan  20635  log2cnv  20644  log2ublem2  20647  log2ublem3  20648  basellem8  20730  ppi1  20807  cht1  20808  chp1  20810  ppi1i  20811  ppi2i  20812  cht2  20815  cht3  20816  bclbnd  20924  bposlem8  20935  wlkntrllem4  21409  constr1trl  21429  2trllem3  21437  constr2trl  21439  constr3trllem3  21480  constr3pthlem1  21483  constr3pthlem3  21485  vdegp1ai  21547  ex-dif  21572  ex-xp  21585  ex-rn  21589  ip0i  22167  ip1ilem  22168  ipdirilem  22171  ipasslem10  22181  hvnegdii  22405  hvaddcani  22408  hvsubaddi  22409  hisubcomi  22447  normlem0  22452  normlem3  22455  normlem9  22461  bcseqi  22463  norm0  22471  norm-ii-i  22480  norm3difi  22490  normpari  22497  normpar2i  22499  polid2i  22500  shs0i  22792  chj0i  22798  pjsslem  23022  ho0subi  23139  hoaddsubi  23165  hosd1i  23166  hopncani  23168  nmop0  23330  nmfn0  23331  lnopunilem1  23354  lnophmlem2  23361  opsqrlem2  23485  pjclem1  23539  atabsi  23745  dmdbr6ati  23767  inin  23833  iuninc  23848  fmptpr  23897  gtiso  23922  dmhashres  23988  recusp  24139  zlmtset  24143  qqhucn  24168  rrhcn  24172  zrhre  24174  qqhre  24175  rrhre  24176  esumnul  24232  mbfmcst  24396  0rrv  24481  coinflipprob  24509  ballotlem2  24518  ballotlemfp1  24521  ballotth  24567  derang0  24627  subfac0  24635  subfac1  24636  dfrdg2  25169  pred0  25216  trpred0  25256  wfrlem14  25286  wfrlem16  25288  symdif0  25385  symdifid  25387  pprodcnveq  25440  dffv5  25480  fullfunfv  25503  ax5seglem7  25581  axlowdimlem8  25595  axlowdimlem11  25598  ellines  25793  rankeq1o  25819  onint1  25906  dvreasin  25973  areacirclem6  25980  heiborlem6  26209  diophrw  26501  dnwech  26807  lmhmlnmsplit  26847  fgraphopab  27191  lhe4.4ex1a  27208  itgsin0pilem1  27405  stoweidlem13  27423  wallispilem4  27478  wallispi2lem1  27481  wallispi2lem2  27482  stirlinglem3  27486  sec0  27842  bnj1416  28739  hdmap1cbv  31969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2373
  Copyright terms: Public domain W3C validator