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

Theorem 3eqtri 2462
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 2458 . 2  |-  B  =  D
51, 4eqtri 2458 1  |-  A  =  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  csbid  3409  un23  3631  in32  3680  unvdif  3875  undif2  3877  undifabs  3878  difun2  3881  difdifdir  3889  dfif4  3930  dfif5  3931  tpidm23  4106  dfopif  4187  unisn  4237  dfiunv2  4338  symdif0  4379  symdifid  4381  unidif0  4598  uniop  4724  xpun  4912  dfrn2  5043  dfdmf  5048  dfrnf  5093  res0  5129  resres  5137  xpssres  5159  dfima2  5190  imai  5200  ima0  5203  imaundir  5269  xpima  5299  dmresv  5314  rescnvcnv  5318  dmtpop  5332  rnsnopg  5335  resdmres  5346  dmmpt  5350  dmco  5363  co01  5370  pred0  5429  suc0  5516  unisuc  5518  iunsuc  5524  fresaun  5771  dffv4  5878  fvssunirn  5904  fpr  6087  fvsnun2  6115  mpt20  6375  dmoprab  6391  rnoprab  6393  elrnmpt2res  6424  ov6g  6448  1st0  6813  2nd0  6814  dfmpt2  6897  curry1  6899  curry2  6902  fpar  6911  algrflem  6916  dftpos2  6998  tposoprab  7017  tposmpt2  7018  fvmpt2curryd  7026  wfrlem14  7057  wfrlem16  7059  dfrecs3  7099  tfrlem8  7110  seqomlem3  7177  df2o3  7203  omxpenlem  7679  dfsdom2  7701  marypha2lem2  7956  scottexs  8357  scott0s  8358  infxpenc2  8451  kmlem3  8580  cdaassen  8610  ackbij1lem2  8649  compsscnv  8799  fin1a2lem12  8839  mulerpqlem  9379  1lt2nq  9397  axi2m1  9582  2p2e4  10727  numsuc  11063  numsucc  11077  xnegmnf  11503  pnfaddmnf  11523  fz0tp  11891  fzo13pr  11994  fzo0to2pr  11995  fzo0to3tp  11996  fzo0to42pr  11997  i4  12374  crreczi  12394  fac1  12460  fac3  12463  hashkf  12514  hashinf  12517  dmhashres  12521  hashun3  12560  cshwsexa  12908  dmtrclfv  13061  abs0  13327  absi  13328  trirecip  13899  geoihalfsum  13916  esum  14113  tan0  14183  coshval  14187  ef01bndlem  14216  3dvds  14347  sadc0  14402  3lcm2e6woprm  14545  6lcm4e12  14546  lcmf0  14569  prmo0  14948  gcdmodi  15000  karatsuba  15010  43prm  15047  139prm  15049  631prm  15052  1259lem1  15056  1259lem2  15057  1259lem3  15058  1259lem4  15059  1259lem5  15060  2503lem1  15062  2503lem2  15063  2503lem3  15064  4001lem2  15067  4001lem3  15068  4001lem4  15069  4001prm  15070  ndxarg  15095  xpsc  15405  pmtrsn  17102  psgnprfval1  17105  sylow2a  17197  0frgp  17355  ablfac1eu  17632  sralem  18326  opsrtoslem2  18634  ply1plusgfvi  18761  pf1rcl  18863  restcld  20110  neitr  20118  txbasval  20543  txindis  20571  cnmpt1st  20605  cnmpt2nd  20606  ufildr  20868  restmetu  21507  reust  22224  ismbl  22348  mbfimaopnlem  22479  itg10  22514  itg2cnlem2  22588  itgz  22606  dvmptid  22779  cos2pi  23287  tan4thpi  23325  sincos6thpi  23326  pige3  23328  dfrelog  23371  logm1  23394  dvlog  23452  efopnlem2  23458  cxpexp  23469  root1id  23550  ang180lem2  23595  1cubrlem  23623  quart1  23638  atandm2  23659  efiasin  23670  asinsinlem  23673  asinsin  23674  asin1  23676  acos1  23677  atancj  23692  atanlogsublem  23697  efiatan2  23699  2efiatan  23700  tanatan  23701  dvatan  23717  log2cnv  23726  log2ublem2  23729  log2ublem3  23730  basellem8  23868  ppi1  23945  cht1  23946  chp1  23948  ppi1i  23949  ppi2i  23950  cht2  23953  cht3  23954  bclbnd  24062  bposlem8  24073  ax5seglem7  24802  axlowdimlem8  24816  axlowdimlem11  24819  wlkntrllem2  25126  constr1trl  25154  constr2spthlem1  25160  constr3trllem3  25216  constr3pthlem1  25219  constr3pthlem3  25221  wlknwwlknvbij  25304  clwwlkvbij  25365  vdegp1ai  25548  ex-dif  25709  ex-xp  25722  ex-rn  25726  ip0i  26302  ip1ilem  26303  ipdirilem  26306  ipasslem10  26316  hvnegdii  26541  hvaddcani  26544  hvsubaddi  26545  hisubcomi  26583  normlem0  26588  normlem3  26591  normlem9  26597  bcseqi  26599  norm0  26607  norm-ii-i  26616  norm3difi  26626  normpari  26633  normpar2i  26635  polid2i  26636  shs0i  26928  chj0i  26934  pjsslem  27158  ho0subi  27274  hoaddsubi  27300  hosd1i  27301  hopncani  27303  nmop0  27465  nmfn0  27466  lnopunilem1  27489  lnophmlem2  27496  opsqrlem2  27620  pjclem1  27674  atabsi  27880  dmdbr6ati  27902  inin  27976  iuninc  28006  gtiso  28112  fpwrelmapffs  28153  lmat22det  28478  ordtcnvNEW  28556  ordtrest2NEW  28559  zlmtset  28599  qqhucn  28626  zrhre  28653  qqhre  28654  esumnul  28699  mbfmcst  28911  carsggect  28970  eulerpartgbij  29022  eulerpartlemn  29031  fib0  29049  fib1  29050  fib2  29052  fib3  29053  fib4  29054  fib5  29055  fib6  29056  0rrv  29101  coinflipprob  29129  ballotlem2  29138  ballotlemfp1  29141  ballotth  29187  signsvf0  29248  bnj1416  29627  derang0  29671  subfac0  29679  subfac1  29680  mthmpps  29999  problem2  30077  quad3  30081  dfrdg2  30220  trpred0  30255  pprodcnveq  30426  dffv5  30467  fullfunfv  30490  ellines  30695  rankeq1o  30714  onint1  30885  bj-xpimasn  31288  bj-pr11val  31339  bj-pr21val  31347  bj-pr22val  31353  bj-nuliotaALT  31363  icorempt2  31479  poimirlem5  31639  poimirlem22  31656  poimirlem26  31660  poimirlem30  31664  mblfinlem2  31672  ismblfin  31675  dvtan  31686  asindmre  31721  dvasin  31722  dvacos  31723  areacirclem5  31730  heiborlem6  31842  hdmap1cbv  35070  diophrw  35300  dnwech  35602  lmhmlnmsplit  35641  fgraphopab  35776  arearect  35789  areaquad  35790  cnvtrrel  35891  dfrcl2  35895  dfrcl4  35897  iunrelexp0  35923  comptiunov2i  35927  relexpaddss  35939  brtrclfv2  35948  trclfvdecomr  35949  corcltrcl  35960  cotrclrcl  35963  xpheOLD  36004  hashnzfz  36296  lhe4.4ex1a  36305  disjinfi  37081  sumnnodd  37272  cosnegpi  37304  itgsin0pilem1  37385  stoweidlem13  37432  wallispilem4  37489  wallispi2lem1  37492  wallispi2lem2  37493  stirlinglem3  37497  dirkertrigeqlem1  37519  fourierdlem56  37584  fourierdlem57  37585  fourierdlem58  37586  fourierdlem62  37590  fourierdlem103  37631  fourierdlem104  37632  fourierdlem112  37640  sqwvfoura  37650  fouriersw  37653  etransclem23  37679  etransclem36  37692  etransclem38  37694  carageniuncllem1  37841  nnsum3primesgbe  38267  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  bgoldbtbndlem1  38280  tgoldbachlt  38289  5tcu2e40  38295  3exp4mod41  38296  41prothprmlem2  38298  41prothprm  38299  cznrnglem  38703  2t6m3t4e0  38879  zlmodzxzldeplem3  39045  sec0  39231
  Copyright terms: Public domain W3C validator