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

Theorem 3eqtri 2340
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 2336 . 2  |-  B  =  D
51, 4eqtri 2336 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1633
This theorem is referenced by:  csbid  3122  un23  3368  in32  3415  dfrab2  3477  undifv  3562  undif2  3564  undifabs  3565  difun2  3567  difdifdir  3575  dfif4  3610  tpidm23  3764  dfopif  3830  unisn  3880  unidif0  4220  uniop  4306  suc0  4503  unisuc  4505  iunsuc  4511  xpun  4784  dfrn2  4905  dfdmf  4910  dfrnf  4954  res0  4996  resres  5005  xpssres  5026  dfima2  5051  imai  5064  ima0  5067  imaundir  5131  dmresv  5169  rescnvcnv  5172  dmtpop  5186  rnsnopg  5189  resdmres  5201  dmmpt  5205  dmco  5218  co01  5224  fresaun  5450  dffv4  5560  fvssunirn  5589  fpr  5742  fvsnun2  5755  dmoprab  5970  rnoprab  5972  ov6g  6027  1st0  6168  2nd0  6169  mpt20  6241  dfmpt2  6251  curry1  6252  curry2  6255  fpar  6264  algrflem  6266  dftpos2  6293  tposoprab  6312  tposmpt2  6313  tfrlem8  6442  seqomlem3  6506  df2o3  6534  omxpenlem  7006  dfsdom2  7027  marypha2lem2  7234  dfsup2OLD  7241  mapfien  7444  scottexs  7602  scott0s  7603  infxpenc2  7694  kmlem3  7823  cdaassen  7853  ackbij1lem2  7892  compsscnv  8042  fin1a2lem12  8082  mulerpqlem  8624  1lt2nq  8642  axi2m1  8826  2p2e4  9889  numsuc  10183  numsucc  10197  xnegmnf  10584  pnfaddmnf  10604  i4  11252  binom2aiOLD  11260  crreczi  11273  fac1  11339  fac3  11342  hashkf  11386  hashinf  11389  hashun3  11413  abs0  11817  absi  11818  trirecip  12368  geoihalfsum  12385  esum  12409  tan0  12478  coshval  12482  ef01bndlem  12511  3dvds  12638  sadc0  12692  gcdmodi  13136  karatsuba  13146  43prm  13170  139prm  13172  631prm  13175  1259lem1  13176  1259lem2  13177  1259lem3  13178  1259lem4  13179  1259lem5  13180  2503lem1  13182  2503lem2  13183  2503lem3  13184  4001lem2  13187  4001lem3  13188  4001lem4  13189  4001prm  13190  ndxarg  13215  xpsc  13508  sylow2a  14979  0frgp  15137  gsumval3  15240  gsumzaddlem  15252  ablfac1eu  15357  opsrtoslem2  16275  ply1plusgfvi  16369  restcld  16959  txbasval  17357  txindis  17384  cnmpt1st  17418  cnmpt2nd  17419  ufildr  17678  ismbl  18938  mbfimaopnlem  19063  itg10  19096  itg2cnlem2  19170  itgz  19188  dvmptid  19359  pf1rcl  19485  cos2pi  19897  tan4thpi  19935  sincos6thpi  19936  pige3  19938  dfrelog  19976  logm1  19995  dvlog  20051  efopnlem2  20057  cxpexp  20068  root1id  20147  ang180lem2  20161  1cubrlem  20190  quart1  20205  atandm2  20226  efiasin  20237  asinsinlem  20240  asinsin  20241  asin1  20243  acos1  20244  atancj  20259  atanlogsublem  20264  efiatan2  20266  2efiatan  20267  tanatan  20268  dvatan  20284  log2cnv  20293  log2ublem2  20296  log2ublem3  20297  basellem8  20378  ppi1  20455  cht1  20456  chp1  20458  ppi1i  20459  ppi2i  20460  cht2  20463  cht3  20464  bclbnd  20572  bposlem8  20583  ex-dif  20863  ex-xp  20876  ex-rn  20880  ip0i  21458  ip1ilem  21459  ipdirilem  21462  ipasslem10  21472  hvnegdii  21696  hvaddcani  21699  hvsubaddi  21700  hisubcomi  21738  normlem0  21743  normlem3  21746  normlem9  21752  bcseqi  21754  norm0  21762  norm-ii-i  21771  norm3difi  21781  normpari  21788  normpar2i  21790  polid2i  21791  shs0i  22083  chj0i  22089  pjsslem  22313  ho0subi  22430  hoaddsubi  22456  hosd1i  22457  hopncani  22459  nmop0  22621  nmfn0  22622  lnopunilem1  22645  lnophmlem2  22652  opsqrlem2  22776  pjclem1  22830  atabsi  23036  dmdbr6ati  23058  inin  23135  iuninc  23154  xpima  23184  fmptpr  23211  gtiso  23238  dmhashres  23306  restmetu  23513  recusp  23535  zlmtset  23546  zrhre  23576  qqhre  23577  esumnul  23619  mbfmcst  23783  0rrv  23883  ballotlem2  23920  ballotlemfp1  23923  ballotth  23969  derang0  23984  subfac0  23992  subfac1  23993  vdegp1ai  24192  gamma1  24480  dfrdg2  24537  pred0  24584  trpred0  24624  wfrlem14  24654  wfrlem16  24656  symdif0  24753  symdifid  24755  pprodcnveq  24808  dffv5  24848  fullfunfv  24871  ax5seglem7  24949  axlowdimlem8  24963  axlowdimlem11  24966  ellines  25161  rankeq1o  25187  onint1  25274  dvreasin  25340  areacirclem6  25347  heiborlem6  25688  diophrw  25986  dnwech  26293  lmhmlnmsplit  26333  fgraphopab  26677  lhe4.4ex1a  26694  stoweidlem13  26910  wallispi2lem1  26968  wallispi2lem2  26969  stirlinglem3  26973  fzo0to2pr  27271  fzo0to3tp  27272  fzo0to42pr  27273  wlkntrllem4  27464  constr1trl  27484  2trllem3  27492  constr2trl  27494  usgrcyclnl2  27525  constr3trllem3  27536  constr3pthlem1  27539  constr3pthlem3  27541  sec0  27679  bnj1416  28580  hdmap1cbv  31811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-ex 1533  df-cleq 2309
  Copyright terms: Public domain W3C validator