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

Theorem 3eqtri 2307
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 2303 . 2  |-  B  =  D
51, 4eqtri 2303 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  csbid  3088  un23  3334  in32  3381  dfrab2  3443  undifv  3528  undif2  3530  undifabs  3531  difun2  3533  difdifdir  3541  dfif4  3576  tpidm23  3730  dfopif  3793  unisn  3843  unidif0  4183  uniop  4269  suc0  4466  unisuc  4468  iunsuc  4474  xpun  4747  dfrn2  4868  dfdmf  4873  dfrnf  4917  res0  4959  resres  4968  xpssres  4989  dfima2  5014  imai  5027  ima0  5030  imaundir  5094  dmresv  5132  rescnvcnv  5135  dmtpop  5149  rnsnopg  5152  resdmres  5164  dmmpt  5168  dmco  5181  co01  5187  fresaun  5412  dffv4  5522  fvssunirn  5551  fpr  5704  fvsnun2  5716  dmoprab  5928  rnoprab  5930  ov6g  5985  1st0  6126  2nd0  6127  mpt20  6199  dfmpt2  6209  curry1  6210  curry2  6213  fpar  6222  algrflem  6224  dftpos2  6251  tposoprab  6270  tposmpt2  6271  tfrlem8  6400  seqomlem3  6464  df2o3  6492  omxpenlem  6963  dfsdom2  6984  marypha2lem2  7189  dfsup2OLD  7196  mapfien  7399  scottexs  7557  scott0s  7558  infxpenc2  7649  kmlem3  7778  cdaassen  7808  ackbij1lem2  7847  compsscnv  7997  fin1a2lem12  8037  mulerpqlem  8579  1lt2nq  8597  axi2m1  8781  2p2e4  9842  numsuc  10136  numsucc  10150  xnegmnf  10537  pnfaddmnf  10557  i4  11205  binom2aiOLD  11213  crreczi  11226  fac1  11292  fac3  11295  hashkf  11339  hashinf  11342  hashun3  11366  abs0  11770  absi  11771  trirecip  12321  geoihalfsum  12338  esum  12362  tan0  12431  coshval  12435  ef01bndlem  12464  3dvds  12591  sadc0  12645  gcdmodi  13089  karatsuba  13099  43prm  13123  139prm  13125  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  2503lem1  13135  2503lem2  13136  2503lem3  13137  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  ndxarg  13168  xpsc  13459  sylow2a  14930  0frgp  15088  gsumval3  15191  gsumzaddlem  15203  ablfac1eu  15308  opsrtoslem2  16226  ply1plusgfvi  16320  restcld  16903  txbasval  17301  txindis  17328  cnmpt1st  17362  cnmpt2nd  17363  ufildr  17626  ismbl  18885  mbfimaopnlem  19010  itg10  19043  itg2cnlem2  19117  itgz  19135  dvmptid  19306  pf1rcl  19432  cos2pi  19844  tan4thpi  19882  sincos6thpi  19883  pige3  19885  dfrelog  19923  logm1  19942  dvlog  19998  efopnlem2  20004  cxpexp  20015  root1id  20094  ang180lem2  20108  1cubrlem  20137  quart1  20152  atandm2  20173  efiasin  20184  asinsinlem  20187  asinsin  20188  asin1  20190  acos1  20191  atancj  20206  atanlogsublem  20211  efiatan2  20213  2efiatan  20214  tanatan  20215  dvatan  20231  log2cnv  20240  log2ublem2  20243  log2ublem3  20244  basellem8  20325  ppi1  20402  cht1  20403  chp1  20405  ppi1i  20406  ppi2i  20407  cht2  20410  cht3  20411  bclbnd  20519  bposlem8  20530  ex-dif  20810  ex-xp  20823  ex-rn  20827  ip0i  21403  ip1ilem  21404  ipdirilem  21407  ipasslem10  21417  hvnegdii  21641  hvaddcani  21644  hvsubaddi  21645  hisubcomi  21683  normlem0  21688  normlem3  21691  normlem9  21697  bcseqi  21699  norm0  21707  norm-ii-i  21716  norm3difi  21726  normpari  21733  normpar2i  21735  polid2i  21736  shs0i  22028  chj0i  22034  pjsslem  22258  ho0subi  22375  hoaddsubi  22401  hosd1i  22402  hopncani  22404  nmop0  22566  nmfn0  22567  lnopunilem1  22590  lnophmlem2  22597  opsqrlem2  22721  pjclem1  22775  atabsi  22981  dmdbr6ati  23003  ballotlem2  23047  ballotlemfp1  23050  ballotth  23096  iuninc  23158  inin  23167  dmhashres  23174  xpima  23202  fmptpr  23214  gtiso  23241  esumnul  23427  mbfmcst  23564  0rrv  23654  derang0  23700  subfac0  23708  subfac1  23709  vdegp1ai  23908  dfrdg2  24152  pred0  24199  trpred0  24239  wfrlem14  24269  wfrlem16  24271  symdif0  24368  symdifid  24370  pprodcnveq  24423  dffv5  24463  fullfunfv  24485  ax5seglem7  24563  axlowdimlem8  24577  axlowdimlem11  24580  ellines  24775  rankeq1o  24801  onint1  24888  dvreasin  24923  areacirclem6  24930  inpc  25277  inposet  25278  ranncnt  25283  dispos  25287  trnij  25615  dfiunv2  25916  cmp2morpdom  25964  cmp2morpcod  25965  intset  26044  heiborlem6  26540  diophrw  26838  dnwech  27145  lmhmlnmsplit  27185  fgraphopab  27529  lhe4.4ex1a  27546  stoweidlem13  27762  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem3  27825  sec0  28230  bnj1416  29069  hdmap1cbv  31993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator