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

Theorem 3eqtri 2851
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 2847 . 2 𝐵 = 𝐷
51, 4eqtri 2847 1 𝐴 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817
This theorem is referenced by:  csbid  3879  un23  4130  in32  4183  dfnul2  4278  unvdif  4406  undif2  4408  undifabs  4409  difun2  4412  difdifdir  4420  dfif4  4465  dfif5  4466  tpidm23  4678  dfopif  4784  dfiunv2  4946  symdif0  4993  symdifid  4995  unidif0  5248  uniop  5393  xpun  5613  dfrn2  5747  dfdmf  5753  dfrnf  5808  res0  5846  resres  5855  xpssres  5878  dfima2  5920  imai  5931  ima0  5934  imaundir  5998  xpima  6028  cnvrescnv  6041  dmresv  6046  rescnvcnv  6050  dmtpop  6064  rnsnopg  6067  resdmres  6078  dmmpt  6083  dmco  6096  co01  6103  suc0  6254  unisuc  6256  iunsuc  6262  fresaun  6541  dffv4  6660  fvssunirn  6692  f1ossf1o  6883  fpr  6909  mpo0  7234  dmoprab  7250  rnoprab  7252  elrnmpores  7283  ov6g  7308  1st0  7692  2nd0  7693  dfmpo  7795  curry1  7797  curry2  7800  fpar  7809  algrflem  7817  dftpos2  7907  tposoprab  7926  tposmpo  7927  fvmpocurryd  7935  wfrlem14  7966  wfrlem16  7968  dfrecs3  8007  tfrlem8  8018  seqomlem3  8086  df2o3  8115  omxpenlem  8616  dfsdom2  8639  marypha2lem2  8899  sup00  8927  epinid0  9063  scottexs  9315  scott0s  9316  infxpenc2  9448  kmlem3  9578  ackbij1lem2  9643  compsscnv  9793  fin1a2lem12  9833  mulerpqlem  10377  1lt2nq  10395  axi2m1  10581  2p2e4  11771  numsuc  12111  numsucc  12137  decmul10add  12166  5p5e10  12168  6p4e10  12169  7p3e10  12172  xnegmnf  12602  pnfaddmnf  12622  fz12pr  12970  fz0tp  13014  fz0to3un2pr  13015  fzo13pr  13127  fzo0to2pr  13128  fzo0to3tp  13129  fzo0to42pr  13130  fzo1to4tp  13131  fldiv4p1lem1div2  13211  sq4e2t8  13569  i4  13574  crreczi  13596  fac1  13644  fac3  13647  hashkf  13699  hashinf  13702  dmhashres  13708  hashun3  13752  cshwsexa  14188  dmtrclfv  14380  abs0  14647  absi  14648  trirecip  15220  geoihalfsum  15240  esum  15436  tan0  15506  coshval  15510  ef01bndlem  15539  3dvds  15682  3dvdsdec  15683  3dvds2dec  15684  sadc0  15803  3lcm2e6woprm  15959  6lcm4e12  15960  lcmf0  15978  prmo0  16372  gcdmodi  16410  karatsuba  16420  43prm  16457  139prm  16459  631prm  16462  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  2503lem1  16472  2503lem2  16473  2503lem3  16474  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  ndxarg  16510  setsfun  16520  setsfun0  16521  pmtrsn  18649  psgnprfval1  18652  sylow2a  18746  ablfac1eu  19197  sralem  19951  opsrtoslem2  20733  ply1plusgfvi  20880  pf1rcl  20982  restcld  21786  neitr  21794  txbasval  22220  txindis  22248  cnmpt1st  22282  cnmpt2nd  22283  ufildr  22545  restmetu  23186  cphipval2  23854  reust  23994  ehl0base  24029  ismbl  24139  mbfimaopnlem  24268  itg10  24301  itg2cnlem2  24375  itgz  24393  dvmptid  24569  cos2pi  25078  tan4thpi  25116  sincos6thpi  25117  pige3ALT  25121  dfrelog  25166  logm1  25189  dvlog  25251  efopnlem2  25257  cxpexp  25268  root1id  25352  sqrt2cxp2logb9e3  25394  ang180lem2  25405  1cubrlem  25436  quart1  25451  atandm2  25472  efiasin  25483  asinsinlem  25486  asinsin  25487  asin1  25489  acos1  25490  atancj  25505  atanlogsublem  25510  efiatan2  25512  2efiatan  25513  tanatan  25514  dvatan  25530  log2cnv  25539  log2ublem2  25542  log2ublem3  25543  birthday  25549  basellem8  25682  cht1  25759  chp1  25761  ppi1i  25762  ppi2i  25763  cht2  25766  cht3  25767  bclbnd  25873  bposlem8  25884  2lgslem3c  25991  2lgslem3d  25992  ax5seglem7  26738  axlowdimlem8  26752  axlowdimlem11  26755  vtxvalsnop  26843  iedgvalsnop  26844  umgrislfupgrlem  26924  usgrexmpledg  27061  usgredgffibi  27123  vdegp1bi  27336  edginwlk  27433  uhgrwkspthlem2  27552  clwwlkvbij  27907  wlk2v2elem2  27950  frgrwopreglem3  28108  ex-dif  28217  ex-xp  28230  ex-rn  28234  ex-lcm  28252  ex-prmo  28253  ip0i  28617  ip1ilem  28618  ipdirilem  28621  ipasslem10  28631  hvnegdii  28854  hvaddcani  28857  hvsubaddi  28858  hisubcomi  28896  normlem0  28901  normlem3  28904  normlem9  28910  bcseqi  28912  norm0  28920  norm-ii-i  28929  norm3difi  28939  normpari  28946  normpar2i  28948  polid2i  28949  shs0i  29241  chj0i  29247  pjsslem  29471  ho0subi  29587  hoaddsubi  29613  hosd1i  29614  hopncani  29616  nmop0  29778  nmfn0  29779  lnopunilem1  29802  lnophmlem2  29809  opsqrlem2  29933  pjclem1  29987  atabsi  30193  dmdbr6ati  30215  inin  30295  iuninc  30330  gtiso  30455  f1od2  30478  fpwrelmapffs  30491  fzodif1  30537  dfdec100  30567  dp20u  30575  dp3mul10  30595  dpmul1000  30596  dpexpp1  30605  dpadd2  30607  dpmul  30610  dpmul4  30611  1mhdrd  30613  cycpmrn  30827  tocyccntz  30828  lmat22det  31155  ordtcnvNEW  31248  ordtrest2NEW  31251  zlmtset  31291  qqhucn  31318  esumnul  31392  mbfmcst  31602  carsggect  31661  eulerpartgbij  31715  eulerpartlemn  31724  fib0  31742  fib1  31743  fib2  31745  fib3  31746  fib4  31747  fib5  31748  fib6  31749  0rrv  31794  coinflipprob  31822  ballotlem2  31831  ballotth  31880  signsvf0  31935  itgexpif  31962  hgt750lem  32007  hgt750lem2  32008  bnj1416  32396  derang0  32501  subfac0  32509  subfac1  32510  satfv1  32695  fmla  32713  fmla0  32714  fmla0xp  32715  fmla1  32719  mthmpps  32914  problem2  32994  quad3  32998  dfrdg2  33125  trpred0  33160  frrlem14  33221  noetalem2  33303  noetalem3  33304  pprodcnveq  33429  dffv5  33470  fullfunfv  33493  ellines  33698  rankeq1o  33717  onint1  33882  bj-xpimasn  34363  bj-pr11val  34413  bj-pr21val  34421  bj-pr22val  34427  bj-nuliotaALT  34447  bj-dfmpoa  34505  bj-opabco  34575  icorempo  34740  finxpreclem4  34783  finxp2o  34788  finxp3o  34789  matunitlindf  35027  poimirlem5  35034  poimirlem22  35051  poimirlem26  35055  poimirlem30  35059  ismblfin  35070  dvtan  35079  asindmre  35112  dvasin  35113  dvacos  35114  areacirclem5  35121  heiborlem6  35226  xrnres4  35785  dfcoels  35807  coss0  35851  refsymrels2  35933  dfeqvrels2  35955  refrelsredund4  35999  hdmap1cbv  39070  lcm4un  39279  lcm5un  39280  lcm6un  39281  lcm7un  39282  lcm8un  39283  5bc2eq10  39319  2xp3dxp2ge1d  39351  imaopab  39374  sqn5ii  39438  decpmul  39440  remul02  39501  sn-1ticom  39528  sn-0lt1  39535  sn-inelr  39538  fltnltalem  39562  diophrw  39644  dnwech  39936  lmhmlnmsplit  39975  fgraphopab  40098  arearect  40109  areaquad  40110  dmnonrel  40234  imanonrel  40237  cononrel1  40238  cononrel2  40239  rclexi  40259  rtrclex  40261  dfrtrcl5  40273  sqrtcval  40285  resqrtvalex  40289  imsqrtvalex  40290  cnvtrrel  40315  dfrcl2  40319  dfrcl4  40321  iunrelexp0  40347  comptiunov2i  40351  relexpaddss  40363  brtrclfv2  40372  trclfvdecomr  40373  corcltrcl  40384  cotrclrcl  40387  fsovcnvlem  40659  neicvgnvo  40765  scottabf  40896  mnuprdlem1  40928  hashnzfz  40972  lhe4.4ex1a  40981  tgqioo2  42137  sumnnodd  42225  limsup0  42289  limsup10ex  42368  liminf10ex  42369  cosnegpi  42462  itgsin0pilem1  42545  stoweidlem13  42608  wallispilem4  42663  wallispi2lem1  42666  wallispi2lem2  42667  stirlinglem3  42671  dirkertrigeqlem1  42693  fourierdlem56  42757  fourierdlem57  42758  fourierdlem58  42759  fourierdlem62  42763  fourierdlem103  42804  fourierdlem104  42805  fourierdlem112  42813  sqwvfoura  42823  fouriersw  42826  etransclem23  42852  etransclem36  42865  etransclem38  42867  carageniuncllem1  43113  0ome  43121  ovn02  43160  smflimlem4  43360  smflim  43363  smflim2  43390  smflimsup  43412  smfliminf  43415  fmtno0  44010  fmtno1  44011  fmtno2  44020  fmtno3  44021  fmtno4  44022  fmtno5lem4  44026  139prmALT  44066  31prm  44067  5tcu2e40  44086  3exp4mod41  44087  41prothprmlem2  44089  41prothprm  44090  nnsum3primesgbe  44263  nnsum4primesodd  44267  nnsum4primesoddALTV  44268  nnsum4primeseven  44271  nnsum4primesevenALTV  44272  bgoldbtbndlem1  44276  tgoldbachlt  44287  cznrnglem  44530  2t6m3t4e0  44703  zlmodzxzldeplem3  44864  ackval0  45047  ackval1  45048  ackval2  45049  ackval3  45050  ackval40  45060  ackval42  45063  ackval50  45065  sec0  45239
  Copyright terms: Public domain W3C validator