Theorem 3eqtri 2648

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

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 |- A = B
2		3eqtri.2	. . 3 |- B = C
3		3eqtri.3	. . 3 |- C = D
4	2, 3	eqtri 2644	. 2 |- B = D
5	1, 4	eqtri 2644	1 |- A = D

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  csbid  3541  un23  3772  in32  3825  unvdif  4042  undif2  4044  undifabs  4045  difun2  4048  difdifdir  4056  dfif4  4101  dfif5  4102  tpidm23  4292  dfopif  4399  unisn  4451  dfiunv2  4556  symdif0  4597  symdifid  4599  unidif0  4838  uniop  4977  xpun  5176  dfrn2  5311  dfdmf  5317  dfrnf  5364  res0  5400  resres  5409  xpssres  5434  dfima2  5468  imai  5478  ima0  5481  imaundir  5546  xpima  5576  dmresv  5593  rescnvcnv  5597  dmtpop  5611  rnsnopg  5614  resdmres  5625  dmmpt  5630  dmco  5643  co01  5650  suc0  5799  unisuc  5801  iunsuc  5807  fresaun  6075  dffv4  6188  fvssunirn  6217  fpr  6421  fvsnun2  6449  mpt20  6725  dmoprab  6741  rnoprab  6743  elrnmpt2res  6774  ov6g  6798  1st0  7174  2nd0  7175  dfmpt2  7267  curry1  7269  curry2  7272  fpar  7281  algrflem  7286  dftpos2  7369  tposoprab  7388  tposmpt2  7389  fvmpt2curryd  7397  wfrlem14  7428  wfrlem16  7430  dfrecs3  7469  tfrlem8  7480  seqomlem3  7547  df2o3  7573  omxpenlem  8061  dfsdom2  8083  marypha2lem2  8342  sup00  8370  scottexs  8750  scott0s  8751  infxpenc2  8845  kmlem3  8974  cdaassen  9004  ackbij1lem2  9043  compsscnv  9193  fin1a2lem12  9233  mulerpqlem  9777  1lt2nq  9795  axi2m1  9980  2p2e4  11144  numsuc  11511  numsucc  11549  decmul10add  11593  decmul10addOLD  11594  5p5e10  11596  6p4e10  11598  7p3e10  11603  xnegmnf  12041  pnfaddmnf  12061  fz0tp  12440  fz0to3un2pr  12441  fzo13pr  12552  fzo0to2pr  12553  fzo0to3tp  12554  fzo0to42pr  12555  fzo1to4tp  12556  sq4e2t8  12962  i4  12967  crreczi  12989  fac1  13064  fac3  13067  hashkf  13119  hashinf  13122  dmhashres  13129  hashun3  13173  cshwsexa  13570  dmtrclfv  13759  abs0  14025  absi  14026  trirecip  14595  geoihalfsum  14614  esum  14811  tan0  14881  coshval  14885  ef01bndlem  14914  3dvds  15052  3dvdsOLD  15053  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  sadc0  15176  3lcm2e6woprm  15328  6lcm4e12  15329  lcmf0  15347  prmo0  15740  gcdmodi  15778  karatsuba  15792  karatsubaOLD  15793  43prm  15829  139prm  15831  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  2503lem1  15844  2503lem2  15845  2503lem3  15846  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  ndxarg  15882  setsfun  15893  setsfun0  15894  xpsc  16217  pmtrsn  17939  psgnprfval1  17942  sylow2a  18034  0frgp  18192  ablfac1eu  18472  sralem  19177  opsrtoslem2  19485  ply1plusgfvi  19612  pf1rcl  19713  restcld  20976  neitr  20984  txbasval  21409  txindis  21437  cnmpt1st  21471  cnmpt2nd  21472  ufildr  21735  restmetu  22375  cphipval2  23040  reust  23169  ismbl  23294  mbfimaopnlem  23422  itg10  23455  itg2cnlem2  23529  itgz  23547  dvmptid  23720  cos2pi  24228  tan4thpi  24266  sincos6thpi  24267  pige3  24269  dfrelog  24312  logm1  24335  dvlog  24397  efopnlem2  24403  cxpexp  24414  root1id  24495  ang180lem2  24540  1cubrlem  24568  quart1  24583  atandm2  24604  efiasin  24615  asinsinlem  24618  asinsin  24619  asin1  24621  acos1  24622  atancj  24637  atanlogsublem  24642  efiatan2  24644  2efiatan  24645  tanatan  24646  dvatan  24662  log2cnv  24671  log2ublem2  24674  log2ublem3  24675  basellem8  24814  cht1  24891  chp1  24893  ppi1i  24894  ppi2i  24895  cht2  24898  cht3  24899  bclbnd  25005  bposlem8  25016  2lgslem3c  25123  2lgslem3d  25124  ax5seglem7  25815  axlowdimlem8  25829  axlowdimlem11  25832  umgrislfupgrlem  26017  usgrexmpledg  26154  usgredgffibi  26216  vdegp1bi  26433  edginwlk  26530  uhgrwkspthlem2  26650  wlksnwwlknvbij  26803  clwwlksvbij  26922  wlk2v2elem2  27016  frgrwopreglem3  27178  ex-dif  27280  ex-xp  27293  ex-rn  27297  ex-lcm  27315  ex-prmo  27316  ip0i  27680  ip1ilem  27681  ipdirilem  27684  ipasslem10  27694  hvnegdii  27919  hvaddcani  27922  hvsubaddi  27923  hisubcomi  27961  normlem0  27966  normlem3  27969  normlem9  27975  bcseqi  27977  norm0  27985  norm-ii-i  27994  norm3difi  28004  normpari  28011  normpar2i  28013  polid2i  28014  shs0i  28308  chj0i  28314  pjsslem  28538  ho0subi  28654  hoaddsubi  28680  hosd1i  28681  hopncani  28683  nmop0  28845  nmfn0  28846  lnopunilem1  28869  lnophmlem2  28876  opsqrlem2  29000  pjclem1  29054  atabsi  29260  dmdbr6ati  29282  inin  29352  iuninc  29379  gtiso  29478  fpwrelmapffs  29509  dfdec100  29576  dp20u  29585  dp3mul10  29606  dpmul1000  29607  dpexpp1  29616  dpadd2  29618  dpmul  29621  dpmul4  29622  1mhdrd  29624  lmat22det  29888  ordtcnvNEW  29966  ordtrest2NEW  29969  zlmtset  30009  qqhucn  30036  zrhre  30063  qqhre  30064  esumnul  30110  mbfmcst  30321  carsggect  30380  eulerpartgbij  30434  eulerpartlemn  30443  fib0  30461  fib1  30462  fib2  30464  fib3  30465  fib4  30466  fib5  30467  fib6  30468  0rrv  30513  coinflipprob  30541  ballotlem2  30550  ballotth  30599  signsvf0  30657  itgexpif  30684  hgt750lem  30729  hgt750lem2  30730  bnj1416  31107  derang0  31151  subfac0  31159  subfac1  31160  mthmpps  31479  problem2  31559  problem2OLD  31560  quad3  31564  dfrdg2  31701  trpred0  31736  noetalem2  31864  noetalem3  31865  pprodcnveq  31990  dffv5  32031  fullfunfv  32054  ellines  32259  rankeq1o  32278  onint1  32448  bj-xpimasn  32942  bj-pr11val  32993  bj-pr21val  33001  bj-pr22val  33007  bj-nuliotaALT  33020  bj-dfmpt2a  33071  icorempt2  33199  finxpreclem4  33231  finxp2o  33236  finxp3o  33237  matunitlindf  33407  poimirlem5  33414  poimirlem22  33431  poimirlem26  33435  poimirlem30  33439  ismblfin  33450  dvtan  33460  asindmre  33495  dvasin  33496  dvacos  33497  areacirclem5  33504  heiborlem6  33615  hdmap1cbv  37092  diophrw  37322  dnwech  37618  lmhmlnmsplit  37657  fgraphopab  37788  arearect  37801  areaquad  37802  dmnonrel  37896  imanonrel  37899  cononrel1  37900  cononrel2  37901  rclexi  37922  dfrtrcl5  37936  cnvtrrel  37962  dfrcl2  37966  dfrcl4  37968  iunrelexp0  37994  comptiunov2i  37998  relexpaddss  38010  brtrclfv2  38019  trclfvdecomr  38020  corcltrcl  38031  cotrclrcl  38034  fsovcnvlem  38307  neicvgnvo  38413  hashnzfz  38519  lhe4.4ex1a  38528  disjinfi  39380  tgqioo2  39774  sumnnodd  39862  limsup0  39926  limsup10ex  40005  liminf10ex  40006  cosnegpi  40078  itgsin0pilem1  40165  stoweidlem13  40230  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem3  40293  dirkertrigeqlem1  40315  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  sqwvfoura  40445  fouriersw  40448  etransclem23  40474  etransclem36  40487  etransclem38  40489  carageniuncllem1  40735  0ome  40743  ovn02  40782  smflimlem4  40982  smflim  40985  smflim2  41012  smflimsup  41034  smfliminf  41037  fmtno0  41452  fmtno1  41453  fmtno2  41462  fmtno3  41463  fmtno4  41464  fmtno5lem4  41468  139prmALT  41511  31prm  41512  5tcu2e40  41532  3exp4mod41  41533  41prothprmlem2  41535  41prothprm  41536  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  tgoldbachlt  41704  tgoldbachltOLD  41710  cznrnglem  41953  2t6m3t4e0  42126  zlmodzxzldeplem3  42291  sec0  42501