Theorem 3eqtri 2787

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 2783	. 2 ⊢ 𝐵 = 𝐷
5	1, 4	eqtri 2783	1 ⊢ 𝐴 = 𝐷

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  csbid  3859  csbconstg  3865  csbie  3881  in32  4126  un23  4172  dfnul4  4280  unvdif  4428  undif2  4430  undifabs  4433  difun2  4436  difdifdir  4446  dfif4  4497  dfif5  4498  tpidm23  4714  dfopif  4836  dfiunv2  4991  symdif0  5044  symdifv  5045  symdifid  5046  unidif0  5320  unidif0OLD  5321  uniop  5487  xpun  5724  dfrn2  5869  dfdmf  5877  dfrnf  5931  res0  5973  resres  5982  xpssres  6006  dfima2  6057  imai  6071  ima0  6074  imaundir  6141  xpima  6173  cnvrescnv  6187  dmresv  6194  rescnvcnv  6205  dmtpop  6219  rnsnopg  6222  resdmres  6233  resdifdi  6237  dmmpt  6241  dmco  6256  co01  6263  relcnvtrg  6268  suc0  6440  iunsuc  6450  fresaun  6754  dffv4  6883  f1ossf1o  7130  fpr  7159  mpo0  7506  dmoprab  7524  rnoprab  7526  elrnmpores  7559  ov6g  7585  1st0  8008  2nd0  8009  f1od2  8111  dfmpo  8116  curry1  8118  curry2  8121  fpar  8130  dftpos2  8264  tposoprab  8283  tposmpo  8284  fvmpocurryd  8292  frrlem14  8321  dfrecs3  8384  tfrlem8  8396  seqomlem3  8466  df2o3  8488  nlim2  8502  omxpenlem  9101  dfsdom2  9123  pwfir  9312  marypha2lem2  9432  sup00  9461  epinid0  9603  scottabf  9943  scottexsOLD  9947  scott0bsOLD  9949  infxpenc2  10105  kmlem3  10235  ackbij1lem2  10302  compsscnv  10453  fin1a2lem12  10493  mulerpqlem  11044  1lt2nq  11062  axi2m1  11248  2p2e4  12481  numsuc  12832  numsucc  12863  decmul10add  12892  5p5e10  12894  6p4e10  12895  7p3e10  12898  xnegmnf  13344  pnfaddmnf  13364  fz12pr  13719  fz0tp  13766  fz0to3un2pr  13767  fz0to4untppr  13768  fz0to5un2tp  13769  fzo13pr  13888  fzo0to2pr  13889  fz01pr  13890  fzo0to3tp  13891  fzo0to42pr  13892  fzo1to4tp  13893  fldiv4p1lem1div2  13979  sq4e2t8  14346  i4  14352  crreczi  14376  fac1  14425  fac3  14428  hashkf  14480  hashinf  14483  dmhashres  14489  hashun3  14532  dmtrclfv  15177  abs0  15458  absi  15459  trirecip  16038  geoihalfsum  16057  esum  16252  tan0  16325  coshval  16329  ef01bndlem  16358  3dvds  16507  3dvdsdec  16508  3dvds2dec  16509  sadc0  16630  3lcm2e6woprm  16796  6lcm4e12  16797  lcmf0  16815  prmo0  17220  prmo3  17225  gcdmodi  17258  karatsuba  17267  43prm  17306  139prm  17308  631prm  17311  1259lem1  17315  1259lem2  17316  1259lem3  17317  1259lem4  17318  1259lem5  17319  2503lem1  17321  2503lem2  17322  2503lem3  17323  4001lem1  17325  4001lem2  17326  4001lem3  17327  4001lem4  17328  setsfun  17355  setsfun0  17356  ndxarg  17380  chnccat  18806  ex-chn2  18818  pmtrsn  19739  psgnprfval1  19742  sylow2a  19839  ablfac1eu  20295  sralem  21457  pzriprng1ALT  21808  opsrtoslem2  22371  ply1plusgfvi  22565  pf1rcl  22673  matunitlindf  23002  restcld  23496  neitr  23504  txbasval  23931  txindis  23959  cnmpt1st  23993  cnmpt2nd  23994  ufildr  24256  restmetu  24895  cphipval2  25568  reust  25708  ehl0base  25743  ismbl  25853  mbfimaopnlem  25982  itg10  26015  itg2cnlem2  26089  itgz  26107  dvmptid  26283  cos2pi  26811  tan4thpi  26849  sincos6thpi  26850  pige3ALT  26854  dfrelog  26899  logm1  26923  dvlog  26985  efopnlem2  26991  cxpexp  27002  root1id  27088  sqrt2cxp2logb9e3  27133  ang180lem2  27144  1cubrlem  27175  quart1  27190  atandm2  27211  efiasin  27222  asinsinlem  27225  asinsin  27226  asin1  27228  acos1  27229  atancj  27244  atanlogsublem  27249  efiatan2  27251  2efiatan  27252  tanatan  27253  dvatan  27269  log2cnv  27278  log2ublem2  27281  log2ublem3  27282  birthday  27288  cht1  27498  chp1  27500  ppi1i  27501  ppi2i  27502  cht2  27505  cht3  27506  bclbnd  27613  bposlem8  27624  2lgslem3c  27731  2lgslem3d  27732  noetasuplem2  28097  noetasuplem3  28098  noetasuplem4  28099  noetainflem4  28103  bday0  28203  old0  28231  new0  28256  left1s  28287  right1s  28288  ltslpss  28300  leslss  28301  mulsproplem13  28520  mulsproplem14  28521  precsexlem1  28599  precsexlem2  28600  oniso  28663  bdayn0sf1o  28762  ax5seglem7  29519  axlowdimlem8  29533  axlowdimlem11  29536  vtxvalsnop  29625  iedgvalsnop  29626  umgrislfupgrlem  29706  usgrexmpledg  29849  usgredgffibi  29911  vdegp1bi  30124  edginwlk  30221  clwwlkvbij  30710  wlk2v2elem2  30763  frgrwopreglem3  30921  ex-dif  31030  ex-xp  31043  ex-rn  31047  ex-lcm  31065  ex-prmo  31066  ip0i  31433  ip1ilem  31434  ipdirilem  31437  ipasslem10  31447  hvnegdii  31670  hvaddcani  31673  hvsubaddi  31674  hisubcomi  31712  normlem0  31717  normlem3  31720  normlem9  31726  bcseqi  31728  norm0  31736  norm-ii-i  31745  norm3difi  31755  normpari  31762  normpar2i  31764  polid2i  31765  shs0i  32057  chj0i  32063  pjsslem  32287  ho0subi  32403  hoaddsubi  32429  hosd1i  32430  hopncani  32432  nmop0  32594  nmfn0  32595  lnopunilem1  32618  lnophmlem2  32625  opsqrlem2  32749  pjclem1  32803  atabsi  33009  dmdbr6ati  33031  inin  33160  iuninc  33203  gtiso  33342  fpwrelmapffs  33373  fzodif1  33431  nn0split01  33456  dfdec100  33468  dp20u  33491  dp3mul10  33511  dpmul1000  33512  dpexpp1  33521  dpadd2  33523  dpmul  33526  dpmul4  33527  1mhdrd  33529  cycpmrn  33751  tocyccntz  33752  cos9thpiminplylem4  34464  cos9thpiminplylem5  34465  lmat22det  34501  ordtcnvNEW  34599  ordtrest2NEW  34602  zlmtset  34642  qqhucn  34671  esumnul  34727  mbfmcst  34938  carsggect  34997  eulerpartgbij  35051  eulerpartlemn  35060  fib0  35078  fib1  35079  fib2  35081  fib3  35082  fib4  35083  fib5  35084  fib6  35085  0rrv  35130  coinflipprob  35159  ballotlem2  35168  ballotth  35217  signsvf0  35256  itgexpif  35282  hgt750lem  35327  hgt750lem2  35328  bnj1416  35716  r11  35778  r12  35779  derang0  36021  subfac0  36029  subfac1  36030  satfv1  36215  fmla  36233  fmla0  36234  fmla0xp  36235  fmla1  36239  mthmpps  36434  problem2  36518  quad3  36522  dfrdg2  36650  pprodcnveq  36738  dffv5  36779  dfsuccf2  36798  fullfunfv  36804  ellines  37010  rankeq1o  37025  onint1  37330  bj-xpimasn  37961  bj-pr11val  38011  bj-pr21val  38019  bj-pr22val  38025  bj-nuliotaALT  38066  bj-dfmpoa  38133  bj-opabco  38203  icorempo  38368  finxpreclem4  38411  finxp2o  38416  finxp3o  38417  poimirlem5  38637  poimirlem22  38654  poimirlem26  38658  poimirlem30  38662  ismblfin  38673  dvtan  38682  asindmre  38715  dvasin  38716  dvacos  38717  areacirclem5  38724  heiborlem6  38844  dmcnvep  39414  dmxrncnvep  39415  dmcnvepres  39416  dmxrnuncnvepres  39418  xrnres4  39454  dfadjliftmap2  39483  blockadjliftmap  39484  dfblockliftmap2  39487  dfsucmap3  39489  dfsuccl2  39496  dfcoels  39546  coss0  39595  refsymrels2  39675  dfeqvrels2  39698  refrelsredund4  39742  hdmap1cbv  42953  lcm4un  43160  lcm5un  43161  lcm6un  43162  lcm7un  43163  lcm8un  43164  3lexlogpow5ineq1  43198  5bc2eq10  43286  imaopab  43379  decpmul  43439  cxpi11d  43488  tan3rdpi  43497  sin2t3rdpi  43498  cos2t3rdpi  43499  readvrec2  43506  remul02  43550  fltnltalem  43767  sum9cubes  43777  diophrw  43864  dnwech  44149  lmhmlnmsplit  44183  fgraphopab  44299  arearect  44311  areaquad  44312  oaomoencom  44413  dmnonrel  44684  imanonrel  44687  cononrel1  44688  cononrel2  44689  rclexi  44709  rtrclex  44711  dfrtrcl5  44723  sqrtcval  44735  resqrtvalex  44739  imsqrtvalex  44740  cnvtrrel  44764  dfrcl2  44768  dfrcl4  44770  iunrelexp0  44796  comptiunov2i  44800  relexpaddss  44812  brtrclfv2  44821  trclfvdecomr  44822  corcltrcl  44833  cotrclrcl  44836  fsovcnvlem  45107  neicvgnvo  45209  k0004val0  45248  mnuprdlem1  45350  hashnzfz  45398  lhe4.4ex1a  45407  tgqioo2  46653  sumnnodd  46736  limsup0  46798  limsup10ex  46877  liminf10ex  46878  cosnegpi  46971  itgsin0pilem1  47054  stoweidlem13  47117  wallispilem4  47172  wallispi2lem1  47175  wallispi2lem2  47176  stirlinglem3  47180  dirkertrigeqlem1  47202  fourierdlem56  47266  fourierdlem57  47267  fourierdlem58  47268  fourierdlem62  47272  fourierdlem103  47313  fourierdlem104  47314  fourierdlem112  47322  sqwvfoura  47332  fouriersw  47335  etransclem23  47361  etransclem36  47374  etransclem38  47376  carageniuncllem1  47625  0ome  47633  ovn02  47672  smflimlem4  47878  smflim  47881  smflim2  47910  smflimsup  47932  smfliminf  47935  numtowerdt  48010  cos5t  48019  goldpolyfactor  48021  goldratmolem2  48027  goldratval  48030  cjnpoly  48033  fmtno0  48719  fmtno1  48720  fmtno2  48729  fmtno3  48730  fmtno4  48731  fmtno5lem4  48735  139prmALT  48775  31prm  48776  5tcu2e40  48794  3exp4mod41  48795  41prothprmlem2  48797  41prothprm  48798  ppivalnn4  48806  nnsum3primesgbe  48984  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  bgoldbtbndlem1  48997  tgoldbachlt  49008  isuspgrim0lem  49085  isubgr3stgrlem4  49161  isubgr3stgrlem6  49163  isubgr3stgrlem7  49164  usgrexmpl1vtx  49215  usgrexmpl1edg  49216  usgrexmpl2vtx  49220  usgrexmpl2edg  49221  gpg5gricstgr3  49282  gpgprismgr4cycllem7  49293  cznrnglem  49450  2t6m3t4e0  49554  zlmodzxzldeplem3  49708  ackval0  49886  ackval1  49887  ackval2  49888  ackval3  49889  ackval40  49899  ackval42  49902  ackval50  49904  ehl2eudisval0  49932  disjdifb  50014  dftpos6  50082  tposresg  50085  tposrescnv  50086  tposres3  50088  tposid  50092  iscnrm3rlem1  50148  dfswapf2  50477  setc1onsubc  50834  parswapprop  50871  par2hom  50873  fuconuniqlem  50875  fuconuniqvalslem  50877  sec0  51022  dvcsc  51026  dvcot  51027