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

Theorem 3eqtri 2677
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 2673 . 2 𝐵 = 𝐷
51, 4eqtri 2673 1 𝐴 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  csbid  3574  un23  3805  in32  3858  unvdif  4075  undif2  4077  undifabs  4078  difun2  4081  difdifdir  4089  dfif4  4134  dfif5  4135  tpidm23  4324  dfopif  4430  unisn  4483  dfiunv2  4588  symdif0  4629  symdifid  4631  unidif0  4868  uniop  5006  xpun  5210  dfrn2  5343  dfdmf  5349  dfrnf  5396  res0  5432  resres  5444  xpssres  5469  dfima2  5503  imai  5513  ima0  5516  imaundir  5581  xpima  5611  dmresv  5628  rescnvcnv  5632  dmtpop  5647  rnsnopg  5650  resdmres  5663  dmmpt  5668  dmco  5681  co01  5688  suc0  5837  unisuc  5839  iunsuc  5845  fresaun  6113  dffv4  6226  fvssunirn  6255  fpr  6461  fvsnun2  6490  mpt20  6767  dmoprab  6783  rnoprab  6785  elrnmpt2res  6816  ov6g  6840  1st0  7216  2nd0  7217  dfmpt2  7312  curry1  7314  curry2  7317  fpar  7326  algrflem  7331  dftpos2  7414  tposoprab  7433  tposmpt2  7434  fvmpt2curryd  7442  wfrlem14  7473  wfrlem16  7475  dfrecs3  7514  tfrlem8  7525  seqomlem3  7592  df2o3  7618  omxpenlem  8102  dfsdom2  8124  marypha2lem2  8383  sup00  8411  scottexs  8788  scott0s  8789  infxpenc2  8883  kmlem3  9012  cdaassen  9042  ackbij1lem2  9081  compsscnv  9231  fin1a2lem12  9271  mulerpqlem  9815  1lt2nq  9833  axi2m1  10018  2p2e4  11182  numsuc  11549  numsucc  11587  decmul10add  11631  decmul10addOLD  11632  5p5e10  11634  6p4e10  11636  7p3e10  11641  xnegmnf  12079  pnfaddmnf  12099  fz0tp  12479  fz0to3un2pr  12480  fzo13pr  12592  fzo0to2pr  12593  fzo0to3tp  12594  fzo0to42pr  12595  fzo1to4tp  12596  sq4e2t8  13002  i4  13007  crreczi  13029  fac1  13104  fac3  13107  hashkf  13159  hashinf  13162  dmhashres  13169  hashun3  13211  cshwsexa  13616  dmtrclfv  13803  abs0  14069  absi  14070  trirecip  14639  geoihalfsum  14658  esum  14855  tan0  14925  coshval  14929  ef01bndlem  14958  3dvds  15099  3dvdsOLD  15100  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  sadc0  15223  3lcm2e6woprm  15375  6lcm4e12  15376  lcmf0  15394  prmo0  15787  gcdmodi  15825  karatsuba  15839  karatsubaOLD  15840  43prm  15876  139prm  15878  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  2503lem1  15891  2503lem2  15892  2503lem3  15893  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  ndxarg  15929  setsfun  15940  setsfun0  15941  xpsc  16264  pmtrsn  17985  psgnprfval1  17988  sylow2a  18080  0frgp  18238  ablfac1eu  18518  sralem  19225  opsrtoslem2  19533  ply1plusgfvi  19660  pf1rcl  19761  restcld  21024  neitr  21032  txbasval  21457  txindis  21485  cnmpt1st  21519  cnmpt2nd  21520  ufildr  21782  restmetu  22422  cphipval2  23086  reust  23215  ismbl  23340  mbfimaopnlem  23467  itg10  23500  itg2cnlem2  23574  itgz  23592  dvmptid  23765  cos2pi  24273  tan4thpi  24311  sincos6thpi  24312  pige3  24314  dfrelog  24357  logm1  24380  dvlog  24442  efopnlem2  24448  cxpexp  24459  root1id  24540  ang180lem2  24585  1cubrlem  24613  quart1  24628  atandm2  24649  efiasin  24660  asinsinlem  24663  asinsin  24664  asin1  24666  acos1  24667  atancj  24682  atanlogsublem  24687  efiatan2  24689  2efiatan  24690  tanatan  24691  dvatan  24707  log2cnv  24716  log2ublem2  24719  log2ublem3  24720  basellem8  24859  cht1  24936  chp1  24938  ppi1i  24939  ppi2i  24940  cht2  24943  cht3  24944  bclbnd  25050  bposlem8  25061  2lgslem3c  25168  2lgslem3d  25169  ax5seglem7  25860  axlowdimlem8  25874  axlowdimlem11  25877  umgrislfupgrlem  26062  usgrexmpledg  26199  usgredgffibi  26261  vdegp1bi  26489  edginwlk  26586  uhgrwkspthlem2  26706  wlksnwwlknvbij  26871  clwwlkvbij  27088  clwwlkvbijOLD  27089  wlk2v2elem2  27134  frgrwopreglem3  27294  ex-dif  27410  ex-xp  27423  ex-rn  27427  ex-lcm  27445  ex-prmo  27446  ip0i  27808  ip1ilem  27809  ipdirilem  27812  ipasslem10  27822  hvnegdii  28047  hvaddcani  28050  hvsubaddi  28051  hisubcomi  28089  normlem0  28094  normlem3  28097  normlem9  28103  bcseqi  28105  norm0  28113  norm-ii-i  28122  norm3difi  28132  normpari  28139  normpar2i  28141  polid2i  28142  shs0i  28436  chj0i  28442  pjsslem  28666  ho0subi  28782  hoaddsubi  28808  hosd1i  28809  hopncani  28811  nmop0  28973  nmfn0  28974  lnopunilem1  28997  lnophmlem2  29004  opsqrlem2  29128  pjclem1  29182  atabsi  29388  dmdbr6ati  29410  inin  29478  iuninc  29505  gtiso  29606  f1od2  29627  fpwrelmapffs  29637  dfdec100  29704  dp20u  29713  dp3mul10  29734  dpmul1000  29735  dpexpp1  29744  dpadd2  29746  dpmul  29749  dpmul4  29750  1mhdrd  29752  lmat22det  30016  ordtcnvNEW  30094  ordtrest2NEW  30097  zlmtset  30137  qqhucn  30164  zrhre  30191  qqhre  30192  esumnul  30238  mbfmcst  30449  carsggect  30508  eulerpartgbij  30562  eulerpartlemn  30571  fib0  30589  fib1  30590  fib2  30592  fib3  30593  fib4  30594  fib5  30595  fib6  30596  0rrv  30641  coinflipprob  30669  ballotlem2  30678  ballotth  30727  signsvf0  30785  itgexpif  30812  hgt750lem  30857  hgt750lem2  30858  bnj1416  31233  derang0  31277  subfac0  31285  subfac1  31286  mthmpps  31605  problem2  31685  problem2OLD  31686  quad3  31690  dfrdg2  31825  trpred0  31860  noetalem2  31989  noetalem3  31990  pprodcnveq  32115  dffv5  32156  fullfunfv  32179  ellines  32384  rankeq1o  32403  onint1  32573  bj-xpimasn  33067  bj-pr11val  33118  bj-pr21val  33126  bj-pr22val  33132  bj-nuliotaALT  33145  bj-dfmpt2a  33196  icorempt2  33329  finxpreclem4  33361  finxp2o  33366  finxp3o  33367  matunitlindf  33537  poimirlem5  33544  poimirlem22  33561  poimirlem26  33565  poimirlem30  33569  ismblfin  33580  dvtan  33590  asindmre  33625  dvasin  33626  dvacos  33627  areacirclem5  33634  heiborlem6  33745  xrnres4  34303  dfcoels  34325  coss0  34369  refsymrels2  34449  hdmap1cbv  37409  diophrw  37639  dnwech  37935  lmhmlnmsplit  37974  fgraphopab  38105  arearect  38118  areaquad  38119  dmnonrel  38213  imanonrel  38216  cononrel1  38217  cononrel2  38218  rclexi  38239  dfrtrcl5  38253  cnvtrrel  38279  dfrcl2  38283  dfrcl4  38285  iunrelexp0  38311  comptiunov2i  38315  relexpaddss  38327  brtrclfv2  38336  trclfvdecomr  38337  corcltrcl  38348  cotrclrcl  38351  fsovcnvlem  38624  neicvgnvo  38730  hashnzfz  38836  lhe4.4ex1a  38845  disjinfi  39694  tgqioo2  40092  sumnnodd  40180  limsup0  40244  limsup10ex  40323  liminf10ex  40324  cosnegpi  40396  itgsin0pilem1  40483  stoweidlem13  40548  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem3  40611  dirkertrigeqlem1  40633  fourierdlem56  40697  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  sqwvfoura  40763  fouriersw  40766  etransclem23  40792  etransclem36  40805  etransclem38  40807  carageniuncllem1  41056  0ome  41064  ovn02  41103  smflimlem4  41303  smflim  41306  smflim2  41333  smflimsup  41355  smfliminf  41358  fmtno0  41777  fmtno1  41778  fmtno2  41787  fmtno3  41788  fmtno4  41789  fmtno5lem4  41793  139prmALT  41836  31prm  41837  5tcu2e40  41857  3exp4mod41  41858  41prothprmlem2  41860  41prothprm  41861  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  tgoldbachlt  42029  tgoldbachltOLD  42035  cznrnglem  42278  2t6m3t4e0  42451  zlmodzxzldeplem3  42616  sec0  42829
  Copyright terms: Public domain W3C validator