Theorem 3eqtri 2766

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

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 ⊢ 𝐴 = 𝐵
2		3eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3		3eqtri.3	. . 3 ⊢ 𝐶 = 𝐷
4	2, 3	eqtri 2762	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2762	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  csbid  3920  csbconstg  3926  csbie  3943  un23  4183  in32  4237  dfnul4  4340  unvdif  4480  undif2  4482  undifabs  4483  difun2  4486  difdifdir  4497  dfif4  4545  dfif5  4546  tpidm23  4761  dfopif  4874  dfiunv2  5039  symdif0  5089  symdifid  5091  unidif0  5365  uniop  5524  xpun  5761  dfrn2  5901  dfdmf  5909  dfrnf  5963  res0  6003  resres  6012  xpssres  6037  dfima2  6081  imai  6093  ima0  6096  imaundir  6172  xpima  6203  cnvrescnv  6216  dmresv  6221  rescnvcnv  6225  dmtpop  6239  rnsnopg  6242  resdmres  6253  resdifdi  6257  dmmpt  6261  dmco  6275  co01  6282  suc0  6460  iunsuc  6470  fresaun  6779  dffv4  6903  fvssunirnOLD  6940  f1ossf1o  7147  fpr  7173  mpo0  7517  dmoprab  7534  rnoprab  7536  elrnmpores  7570  ov6g  7596  1st0  8018  2nd0  8019  dfmpo  8125  curry1  8127  curry2  8130  fpar  8139  dftpos2  8266  tposoprab  8285  tposmpo  8286  fvmpocurryd  8294  frrlem14  8322  dfwrecsOLD  8336  wfrlem14OLD  8360  wfrlem16OLD  8362  dfrecs3  8410  dfrecs3OLD  8411  tfrlem8  8422  seqomlem3  8490  df2o3  8512  nlim2  8526  omxpenlem  9111  dfsdom2  9134  pwfir  9352  marypha2lem2  9473  sup00  9501  epinid0  9637  scottexs  9924  scott0s  9925  infxpenc2  10059  kmlem3  10190  ackbij1lem2  10257  compsscnv  10408  fin1a2lem12  10448  mulerpqlem  10992  1lt2nq  11010  axi2m1  11196  2p2e4  12398  numsuc  12744  numsucc  12770  decmul10add  12799  5p5e10  12801  6p4e10  12802  7p3e10  12805  xnegmnf  13248  pnfaddmnf  13268  fz12pr  13617  fz0tp  13664  fz0to3un2pr  13665  fz0to4untppr  13666  fz0to5un2tp  13667  fzo13pr  13784  fzo0to2pr  13785  fz01pr  13786  fzo0to3tp  13787  fzo0to42pr  13788  fzo1to4tp  13789  fldiv4p1lem1div2  13871  sq4e2t8  14234  i4  14239  crreczi  14263  fac1  14312  fac3  14315  hashkf  14367  hashinf  14370  dmhashres  14376  hashun3  14419  cshwsexaOLD  14859  dmtrclfv  15053  abs0  15320  absi  15321  trirecip  15895  geoihalfsum  15914  esum  16112  tan0  16183  coshval  16187  ef01bndlem  16216  3dvds  16364  3dvdsdec  16365  3dvds2dec  16366  sadc0  16487  3lcm2e6woprm  16648  6lcm4e12  16649  lcmf0  16667  prmo0  17069  gcdmodi  17107  karatsuba  17117  43prm  17155  139prm  17157  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  2503lem1  17170  2503lem2  17171  2503lem3  17172  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  setsfun  17204  setsfun0  17205  ndxarg  17229  pmtrsn  19551  psgnprfval1  19554  sylow2a  19651  ablfac1eu  20107  sralem  21192  sralemOLD  21193  pzriprng1ALT  21524  opsrtoslem2  22097  ply1plusgfvi  22258  pf1rcl  22368  restcld  23195  neitr  23203  txbasval  23629  txindis  23657  cnmpt1st  23691  cnmpt2nd  23692  ufildr  23954  restmetu  24598  cphipval2  25288  reust  25428  ehl0base  25463  ismbl  25574  mbfimaopnlem  25703  itg10  25736  itg2cnlem2  25811  itgz  25830  dvmptid  26009  cos2pi  26532  tan4thpi  26570  tan4thpiOLD  26571  sincos6thpi  26572  pige3ALT  26576  dfrelog  26621  logm1  26645  dvlog  26707  efopnlem2  26713  cxpexp  26724  root1id  26811  sqrt2cxp2logb9e3  26856  ang180lem2  26867  1cubrlem  26898  quart1  26913  atandm2  26934  efiasin  26945  asinsinlem  26948  asinsin  26949  asin1  26951  acos1  26952  atancj  26967  atanlogsublem  26972  efiatan2  26974  2efiatan  26975  tanatan  26976  dvatan  26992  log2cnv  27001  log2ublem2  27004  log2ublem3  27005  birthday  27011  basellem8  27145  cht1  27222  chp1  27224  ppi1i  27225  ppi2i  27226  cht2  27229  cht3  27230  bclbnd  27338  bposlem8  27349  2lgslem3c  27456  2lgslem3d  27457  noetasuplem2  27793  noetasuplem3  27794  noetasuplem4  27795  noetainflem4  27799  bday0s  27887  old0  27912  new0  27927  left1s  27947  right1s  27948  sltlpss  27959  slelss  27960  mulsproplem13  28168  mulsproplem14  28169  precsexlem1  28245  precsexlem2  28246  ax5seglem7  28964  axlowdimlem8  28978  axlowdimlem11  28981  vtxvalsnop  29072  iedgvalsnop  29073  umgrislfupgrlem  29153  usgrexmpledg  29293  usgredgffibi  29355  vdegp1bi  29569  edginwlk  29667  uhgrwkspthlem2  29786  clwwlkvbij  30141  wlk2v2elem2  30184  frgrwopreglem3  30342  ex-dif  30451  ex-xp  30464  ex-rn  30468  ex-lcm  30486  ex-prmo  30487  ip0i  30853  ip1ilem  30854  ipdirilem  30857  ipasslem10  30867  hvnegdii  31090  hvaddcani  31093  hvsubaddi  31094  hisubcomi  31132  normlem0  31137  normlem3  31140  normlem9  31146  bcseqi  31148  norm0  31156  norm-ii-i  31165  norm3difi  31175  normpari  31182  normpar2i  31184  polid2i  31185  shs0i  31477  chj0i  31483  pjsslem  31707  ho0subi  31823  hoaddsubi  31849  hosd1i  31850  hopncani  31852  nmop0  32014  nmfn0  32015  lnopunilem1  32038  lnophmlem2  32045  opsqrlem2  32169  pjclem1  32223  atabsi  32429  dmdbr6ati  32451  inin  32543  iuninc  32580  gtiso  32715  f1od2  32738  fpwrelmapffs  32751  fzodif1  32800  nn0split01  32823  dfdec100  32836  dp20u  32844  dp3mul10  32864  dpmul1000  32865  dpexpp1  32874  dpadd2  32876  dpmul  32879  dpmul4  32880  1mhdrd  32882  cycpmrn  33145  tocyccntz  33146  lmat22det  33782  ordtcnvNEW  33880  ordtrest2NEW  33883  zlmtset  33924  zlmtsetOLD  33925  qqhucn  33954  esumnul  34028  mbfmcst  34240  carsggect  34299  eulerpartgbij  34353  eulerpartlemn  34362  fib0  34380  fib1  34381  fib2  34383  fib3  34384  fib4  34385  fib5  34386  fib6  34387  0rrv  34432  coinflipprob  34460  ballotlem2  34469  ballotth  34518  signsvf0  34573  itgexpif  34599  hgt750lem  34644  hgt750lem2  34645  bnj1416  35031  derang0  35153  subfac0  35161  subfac1  35162  satfv1  35347  fmla  35365  fmla0  35366  fmla0xp  35367  fmla1  35371  mthmpps  35566  problem2  35650  quad3  35654  dfrdg2  35776  pprodcnveq  35864  dffv5  35905  fullfunfv  35928  ellines  36133  rankeq1o  36152  onint1  36431  bj-xpimasn  36937  bj-pr11val  36987  bj-pr21val  36995  bj-pr22val  37001  bj-nuliotaALT  37040  bj-dfmpoa  37100  bj-opabco  37170  icorempo  37333  finxpreclem4  37376  finxp2o  37381  finxp3o  37382  matunitlindf  37604  poimirlem5  37611  poimirlem22  37628  poimirlem26  37632  poimirlem30  37636  ismblfin  37647  dvtan  37656  asindmre  37689  dvasin  37690  dvacos  37691  areacirclem5  37698  heiborlem6  37802  xrnres4  38386  dfcoels  38411  coss0  38460  refsymrels2  38546  dfeqvrels2  38569  refrelsredund4  38613  hdmap1cbv  41784  lcm4un  41997  lcm5un  41998  lcm6un  41999  lcm7un  42000  lcm8un  42001  3lexlogpow5ineq1  42035  5bc2eq10  42123  2xp3dxp2ge1d  42222  imaopab  42248  decpmul  42301  cxpi11d  42357  tan3rdpi  42364  readvrec2  42369  remul02  42411  fltnltalem  42648  sum9cubes  42658  diophrw  42746  dnwech  43036  lmhmlnmsplit  43075  fgraphopab  43191  arearect  43203  areaquad  43204  oaomoencom  43306  dmnonrel  43579  imanonrel  43582  cononrel1  43583  cononrel2  43584  rclexi  43604  rtrclex  43606  dfrtrcl5  43618  sqrtcval  43630  resqrtvalex  43634  imsqrtvalex  43635  cnvtrrel  43659  dfrcl2  43663  dfrcl4  43665  iunrelexp0  43691  comptiunov2i  43695  relexpaddss  43707  brtrclfv2  43716  trclfvdecomr  43717  corcltrcl  43728  cotrclrcl  43731  fsovcnvlem  44002  neicvgnvo  44104  scottabf  44235  mnuprdlem1  44267  hashnzfz  44315  lhe4.4ex1a  44324  tgqioo2  45499  sumnnodd  45585  limsup0  45649  limsup10ex  45728  liminf10ex  45729  cosnegpi  45822  itgsin0pilem1  45905  stoweidlem13  45968  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem3  46031  dirkertrigeqlem1  46053  fourierdlem56  46117  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  sqwvfoura  46183  fouriersw  46186  etransclem23  46212  etransclem36  46225  etransclem38  46227  carageniuncllem1  46476  0ome  46484  ovn02  46523  smflimlem4  46729  smflim  46732  smflim2  46761  smflimsup  46783  smfliminf  46786  fmtno0  47464  fmtno1  47465  fmtno2  47474  fmtno3  47475  fmtno4  47476  fmtno5lem4  47480  139prmALT  47520  31prm  47521  5tcu2e40  47539  3exp4mod41  47540  41prothprmlem2  47542  41prothprm  47543  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem1  47729  tgoldbachlt  47740  isuspgrim0lem  47808  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  usgrexmpl1vtx  47917  usgrexmpl1edg  47918  usgrexmpl2vtx  47922  usgrexmpl2edg  47923  gpg5gricstgr3  47973  cznrnglem  48102  2t6m3t4e0  48192  zlmodzxzldeplem3  48347  ackval0  48529  ackval1  48530  ackval2  48531  ackval3  48532  ackval40  48542  ackval42  48545  ackval50  48547  disjdifb  48657  iscnrm3rlem1  48736  mndtchom  48892  sec0  48990