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

Theorem 3eqtri 2845
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
Hypotheses
Ref Expression
3eqtri.1 𝐴 = 𝐵
3eqtri.2 𝐵 = 𝐶
3eqtri.3 𝐶 = 𝐷
Assertion
Ref Expression
3eqtri 𝐴 = 𝐷

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2 𝐴 = 𝐵
2 3eqtri.2 . . 3 𝐵 = 𝐶
3 3eqtri.3 . . 3 𝐶 = 𝐷
42, 3eqtri 2841 . 2 𝐵 = 𝐷
51, 4eqtri 2841 1 𝐴 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  csbid  3893  un23  4141  in32  4195  dfnul2  4290  unvdif  4419  undif2  4421  undifabs  4422  difun2  4425  difdifdir  4433  dfif4  4478  dfif5  4479  tpidm23  4685  dfopif  4792  dfiunv2  4951  symdif0  4998  symdifid  5000  unidif0  5251  uniop  5396  xpun  5618  dfrn2  5752  dfdmf  5758  dfrnf  5813  res0  5850  resres  5859  xpssres  5882  dfima2  5924  imai  5935  ima0  5938  imaundir  6002  xpima  6032  cnvrescnv  6045  dmresv  6050  rescnvcnv  6054  dmtpop  6068  rnsnopg  6071  resdmres  6082  dmmpt  6087  dmco  6100  co01  6107  suc0  6258  unisuc  6260  iunsuc  6266  fresaun  6542  dffv4  6660  fvssunirn  6692  f1ossf1o  6882  fpr  6908  mpo0  7228  dmoprab  7244  rnoprab  7246  elrnmpores  7277  ov6g  7301  1st0  7684  2nd0  7685  dfmpo  7786  curry1  7788  curry2  7791  fpar  7800  algrflem  7808  dftpos2  7898  tposoprab  7917  tposmpo  7918  fvmpocurryd  7926  wfrlem14  7957  wfrlem16  7959  dfrecs3  7998  tfrlem8  8009  seqomlem3  8077  df2o3  8106  omxpenlem  8606  dfsdom2  8628  marypha2lem2  8888  sup00  8916  epinid0  9052  scottexs  9304  scott0s  9305  infxpenc2  9436  kmlem3  9566  ackbij1lem2  9631  compsscnv  9781  fin1a2lem12  9821  mulerpqlem  10365  1lt2nq  10383  axi2m1  10569  2p2e4  11760  numsuc  12100  numsucc  12126  decmul10add  12155  5p5e10  12157  6p4e10  12158  7p3e10  12161  xnegmnf  12591  pnfaddmnf  12611  fz12pr  12952  fz0tp  12996  fz0to3un2pr  12997  fzo13pr  13109  fzo0to2pr  13110  fzo0to3tp  13111  fzo0to42pr  13112  fzo1to4tp  13113  fldiv4p1lem1div2  13193  sq4e2t8  13550  i4  13555  crreczi  13577  fac1  13625  fac3  13628  hashkf  13680  hashinf  13683  dmhashres  13689  hashun3  13733  cshwsexa  14174  dmtrclfv  14366  abs0  14633  absi  14634  trirecip  15206  geoihalfsum  15226  esum  15422  tan0  15492  coshval  15496  ef01bndlem  15525  3dvds  15668  3dvdsdec  15669  3dvds2dec  15670  sadc0  15791  3lcm2e6woprm  15947  6lcm4e12  15948  lcmf0  15966  prmo0  16360  gcdmodi  16398  karatsuba  16408  43prm  16443  139prm  16445  631prm  16448  1259lem1  16452  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  2503lem1  16458  2503lem2  16459  2503lem3  16460  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  ndxarg  16496  setsfun  16506  setsfun0  16507  pmtrsn  18576  psgnprfval1  18579  sylow2a  18673  ablfac1eu  19124  sralem  19878  opsrtoslem2  20193  ply1plusgfvi  20338  pf1rcl  20440  restcld  21708  neitr  21716  txbasval  22142  txindis  22170  cnmpt1st  22204  cnmpt2nd  22205  ufildr  22467  restmetu  23107  cphipval2  23771  reust  23911  ehl0base  23946  ismbl  24054  mbfimaopnlem  24183  itg10  24216  itg2cnlem2  24290  itgz  24308  dvmptid  24481  cos2pi  24989  tan4thpi  25027  sincos6thpi  25028  pige3ALT  25032  dfrelog  25076  logm1  25099  dvlog  25161  efopnlem2  25167  cxpexp  25178  root1id  25262  sqrt2cxp2logb9e3  25304  ang180lem2  25315  1cubrlem  25346  quart1  25361  atandm2  25382  efiasin  25393  asinsinlem  25396  asinsin  25397  asin1  25399  acos1  25400  atancj  25415  atanlogsublem  25420  efiatan2  25422  2efiatan  25423  tanatan  25424  dvatan  25440  log2cnv  25449  log2ublem2  25452  log2ublem3  25453  birthday  25459  basellem8  25592  cht1  25669  chp1  25671  ppi1i  25672  ppi2i  25673  cht2  25676  cht3  25677  bclbnd  25783  bposlem8  25794  2lgslem3c  25901  2lgslem3d  25902  ax5seglem7  26648  axlowdimlem8  26662  axlowdimlem11  26665  vtxvalsnop  26753  iedgvalsnop  26754  umgrislfupgrlem  26834  usgrexmpledg  26971  usgredgffibi  27033  vdegp1bi  27246  edginwlk  27343  uhgrwkspthlem2  27462  clwwlkvbij  27819  wlk2v2elem2  27862  frgrwopreglem3  28020  ex-dif  28129  ex-xp  28142  ex-rn  28146  ex-lcm  28164  ex-prmo  28165  ip0i  28529  ip1ilem  28530  ipdirilem  28533  ipasslem10  28543  hvnegdii  28766  hvaddcani  28769  hvsubaddi  28770  hisubcomi  28808  normlem0  28813  normlem3  28816  normlem9  28822  bcseqi  28824  norm0  28832  norm-ii-i  28841  norm3difi  28851  normpari  28858  normpar2i  28860  polid2i  28861  shs0i  29153  chj0i  29159  pjsslem  29383  ho0subi  29499  hoaddsubi  29525  hosd1i  29526  hopncani  29528  nmop0  29690  nmfn0  29691  lnopunilem1  29714  lnophmlem2  29721  opsqrlem2  29845  pjclem1  29899  atabsi  30105  dmdbr6ati  30127  inin  30204  iuninc  30240  gtiso  30362  f1od2  30383  fpwrelmapffs  30396  fzodif1  30442  dfdec100  30473  dp20u  30481  dp3mul10  30501  dpmul1000  30502  dpexpp1  30511  dpadd2  30513  dpmul  30516  dpmul4  30517  1mhdrd  30519  cycpmrn  30712  tocyccntz  30713  lmat22det  30986  ordtcnvNEW  31062  ordtrest2NEW  31065  zlmtset  31105  qqhucn  31132  esumnul  31206  mbfmcst  31416  carsggect  31475  eulerpartgbij  31529  eulerpartlemn  31538  fib0  31556  fib1  31557  fib2  31559  fib3  31560  fib4  31561  fib5  31562  fib6  31563  0rrv  31608  coinflipprob  31636  ballotlem2  31645  ballotth  31694  signsvf0  31749  itgexpif  31776  hgt750lem  31821  hgt750lem2  31822  bnj1416  32208  derang0  32313  subfac0  32321  subfac1  32322  satfv1  32507  fmla  32525  fmla0  32526  fmla0xp  32527  fmla1  32531  mthmpps  32726  problem2  32806  quad3  32810  dfrdg2  32937  trpred0  32972  frrlem14  33033  noetalem2  33115  noetalem3  33116  pprodcnveq  33241  dffv5  33282  fullfunfv  33305  ellines  33510  rankeq1o  33529  onint1  33694  bj-xpimasn  34164  bj-pr11val  34214  bj-pr21val  34222  bj-pr22val  34228  bj-nuliotaALT  34245  bj-dfmpoa  34302  icorempo  34514  finxpreclem4  34557  finxp2o  34562  finxp3o  34563  matunitlindf  34771  poimirlem5  34778  poimirlem22  34795  poimirlem26  34799  poimirlem30  34803  ismblfin  34814  dvtan  34823  asindmre  34858  dvasin  34859  dvacos  34860  areacirclem5  34867  heiborlem6  34975  xrnres4  35533  dfcoels  35555  coss0  35599  refsymrels2  35681  dfeqvrels2  35703  refrelsredund4  35747  hdmap1cbv  38818  imaopab  38997  sqn5ii  39050  decpmul  39052  remul02  39113  sn-0lt1  39124  fltnltalem  39152  diophrw  39234  dnwech  39526  lmhmlnmsplit  39565  fgraphopab  39688  arearect  39700  areaquad  39701  dmnonrel  39828  imanonrel  39831  cononrel1  39832  cononrel2  39833  rclexi  39853  rtrclex  39855  dfrtrcl5  39867  cnvtrrel  39893  dfrcl2  39897  dfrcl4  39899  iunrelexp0  39925  comptiunov2i  39929  relexpaddss  39941  brtrclfv2  39950  trclfvdecomr  39951  corcltrcl  39962  cotrclrcl  39965  fsovcnvlem  40237  neicvgnvo  40343  scottabf  40453  mnuprdlem1  40485  hashnzfz  40529  lhe4.4ex1a  40538  disjinfi  41330  tgqioo2  41699  sumnnodd  41787  limsup0  41851  limsup10ex  41930  liminf10ex  41931  cosnegpi  42024  itgsin0pilem1  42111  stoweidlem13  42175  wallispilem4  42230  wallispi2lem1  42233  wallispi2lem2  42234  stirlinglem3  42238  dirkertrigeqlem1  42260  fourierdlem56  42324  fourierdlem57  42325  fourierdlem58  42326  fourierdlem62  42330  fourierdlem103  42371  fourierdlem104  42372  fourierdlem112  42380  sqwvfoura  42390  fouriersw  42393  etransclem23  42419  etransclem36  42432  etransclem38  42434  carageniuncllem1  42680  0ome  42688  ovn02  42727  smflimlem4  42927  smflim  42930  smflim2  42957  smflimsup  42979  smfliminf  42982  fmtno0  43579  fmtno1  43580  fmtno2  43589  fmtno3  43590  fmtno4  43591  fmtno5lem4  43595  139prmALT  43636  31prm  43637  5tcu2e40  43657  3exp4mod41  43658  41prothprmlem2  43660  41prothprm  43661  nnsum3primesgbe  43834  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  bgoldbtbndlem1  43847  tgoldbachlt  43858  cznrnglem  44152  2t6m3t4e0  44324  zlmodzxzldeplem3  44485  sec0  44787
  Copyright terms: Public domain W3C validator