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

Theorem 3eqtri 2466
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 2462 . 2  |-  B  =  D
51, 4eqtri 2462 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1653
This theorem is referenced by:  csbid  3274  un23  3492  in32  3538  dfrab2  3601  unvdif  3726  undif2  3728  undifabs  3729  difun2  3731  difdifdir  3739  dfif4  3774  dfif5  3775  tpidm23  3931  dfopif  4005  unisn  4055  dfiunv2  4151  unidif0  4401  uniop  4488  suc0  4684  unisuc  4686  iunsuc  4692  xpun  4964  dfrn2  5088  dfdmf  5093  dfrnf  5137  res0  5179  resres  5188  xpssres  5209  dfima2  5234  imai  5247  ima0  5250  imaundir  5314  xpima  5342  dmresv  5358  rescnvcnv  5361  dmtpop  5375  rnsnopg  5378  resdmres  5390  dmmpt  5394  dmco  5407  co01  5413  fresaun  5643  dffv4  5754  fvssunirn  5783  fpr  5943  fvsnun2  5958  dmoprab  6183  rnoprab  6185  ov6g  6240  1st0  6382  2nd0  6383  mpt20  6456  dfmpt2  6466  curry1  6467  curry2  6470  fpar  6479  algrflem  6484  dftpos2  6525  tposoprab  6544  tposmpt2  6545  tfrlem8  6674  seqomlem3  6738  df2o3  6766  omxpenlem  7238  dfsdom2  7259  marypha2lem2  7470  dfsup2OLD  7477  mapfien  7682  scottexs  7842  scott0s  7843  infxpenc2  7934  kmlem3  8063  cdaassen  8093  ackbij1lem2  8132  compsscnv  8282  fin1a2lem12  8322  mulerpqlem  8863  1lt2nq  8881  axi2m1  9065  2p2e4  10129  numsuc  10425  numsucc  10439  xnegmnf  10827  pnfaddmnf  10847  fz0tp  11134  fzo0to2pr  11215  fzo0to3tp  11216  fzo0to42pr  11217  i4  11514  binom2aiOLD  11522  crreczi  11535  fac1  11601  fac3  11604  hashkf  11651  hashinf  11654  hashun3  11689  abs0  12121  absi  12122  trirecip  12673  geoihalfsum  12690  esum  12714  tan0  12783  coshval  12787  ef01bndlem  12816  3dvds  12943  sadc0  12997  gcdmodi  13441  karatsuba  13451  43prm  13475  139prm  13477  631prm  13480  1259lem1  13481  1259lem2  13482  1259lem3  13483  1259lem4  13484  1259lem5  13485  2503lem1  13487  2503lem2  13488  2503lem3  13489  4001lem2  13492  4001lem3  13493  4001lem4  13494  4001prm  13495  ndxarg  13520  xpsc  13813  sylow2a  15284  0frgp  15442  gsumval3  15545  gsumzaddlem  15557  ablfac1eu  15662  opsrtoslem2  16576  ply1plusgfvi  16667  restcld  17267  neitr  17275  txbasval  17669  txindis  17697  cnmpt1st  17731  cnmpt2nd  17732  ufildr  17994  restmetu  18648  ismbl  19453  mbfimaopnlem  19576  itg10  19609  itg2cnlem2  19683  itgz  19701  dvmptid  19874  pf1rcl  20000  cos2pi  20415  tan4thpi  20453  sincos6thpi  20454  pige3  20456  dfrelog  20494  logm1  20514  dvlog  20573  efopnlem2  20579  cxpexp  20590  root1id  20669  ang180lem2  20683  1cubrlem  20712  quart1  20727  atandm2  20748  efiasin  20759  asinsinlem  20762  asinsin  20763  asin1  20765  acos1  20766  atancj  20781  atanlogsublem  20786  efiatan2  20788  2efiatan  20789  tanatan  20790  dvatan  20806  log2cnv  20815  log2ublem2  20818  log2ublem3  20819  basellem8  20901  ppi1  20978  cht1  20979  chp1  20981  ppi1i  20982  ppi2i  20983  cht2  20986  cht3  20987  bclbnd  21095  bposlem8  21106  wlkntrllem2  21591  constr1trl  21619  constr2spthlem1  21625  constr3trllem3  21670  constr3pthlem1  21673  constr3pthlem3  21675  vdegp1ai  21737  ex-dif  21762  ex-xp  21775  ex-rn  21779  ip0i  22357  ip1ilem  22358  ipdirilem  22361  ipasslem10  22371  hvnegdii  22595  hvaddcani  22598  hvsubaddi  22599  hisubcomi  22637  normlem0  22642  normlem3  22645  normlem9  22651  bcseqi  22653  norm0  22661  norm-ii-i  22670  norm3difi  22680  normpari  22687  normpar2i  22689  polid2i  22690  shs0i  22982  chj0i  22988  pjsslem  23212  ho0subi  23329  hoaddsubi  23355  hosd1i  23356  hopncani  23358  nmop0  23520  nmfn0  23521  lnopunilem1  23544  lnophmlem2  23551  opsqrlem2  23675  pjclem1  23729  atabsi  23935  dmdbr6ati  23957  inin  24027  iuninc  24042  fmptpr  24093  gtiso  24119  dmhashres  24188  reust  24375  zlmtset  24380  qqhucn  24407  rrhcn  24411  zrhre  24416  qqhre  24417  rrhre  24418  esumnul  24474  mbfmcst  24640  0rrv  24740  coinflipprob  24768  ballotlem2  24777  ballotlemfp1  24780  ballotth  24826  derang0  24886  subfac0  24894  subfac1  24895  dfrdg2  25454  pred0  25505  trpred0  25545  wfrlem14  25582  wfrlem16  25584  symdif0  25700  symdifid  25702  pprodcnveq  25759  dffv5  25800  fullfunfv  25823  ax5seglem7  25905  axlowdimlem8  25919  axlowdimlem11  25922  ellines  26117  rankeq1o  26143  onint1  26230  mblfinlem2  26280  ismblfin  26283  dvtan  26293  dvreasin  26328  areacirclem5  26334  heiborlem6  26563  diophrw  26855  dnwech  27161  lmhmlnmsplit  27200  fgraphopab  27544  lhe4.4ex1a  27561  itgsin0pilem1  27758  stoweidlem13  27776  wallispilem4  27831  wallispi2lem1  27834  wallispi2lem2  27835  stirlinglem3  27839  sec0  28601  bnj1416  29506  hdmap1cbv  32699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2435
  Copyright terms: Public domain W3C validator