Theorem 3eqtri 2792

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  csbid  3867  csbconstg  3873  csbie  3889  un23  4127  in32  4182  dfnul4  4288  unvdif  4436  undif2  4438  undifabs  4441  difun2  4444  difdifdir  4454  dfif4  4505  dfif5  4506  tpidm23  4725  dfopif  4837  dfiunv2  5000  symdif0  5053  symdifv  5054  symdifid  5055  unidif0  5332  unidif0OLD  5333  uniop  5500  xpun  5737  dfrn2  5880  dfdmf  5888  dfrnf  5942  res0  5984  resres  5993  xpssres  6019  dfima2  6066  imai  6078  ima0  6081  imaundir  6150  xpima  6182  cnvrescnv  6196  dmresv  6201  rescnvcnv  6207  dmtpop  6221  rnsnopg  6224  resdmres  6235  resdifdi  6239  dmmpt  6243  dmco  6258  co01  6265  relcnvtrg  6270  suc0  6442  iunsuc  6452  fresaun  6753  dffv4  6882  f1ossf1o  7128  fpr  7155  mpo0  7501  dmoprab  7519  rnoprab  7521  elrnmpores  7554  ov6g  7580  1st0  7994  2nd0  7995  dfmpo  8099  curry1  8101  curry2  8104  fpar  8113  dftpos2  8241  tposoprab  8260  tposmpo  8261  fvmpocurryd  8269  frrlem14  8298  dfrecs3  8361  tfrlem8  8373  seqomlem3  8441  df2o3  8463  nlim2  8477  omxpenlem  9069  dfsdom2  9091  pwfir  9279  marypha2lem2  9399  sup00  9428  epinid0  9570  scottabf  9871  scottexsOLD  9875  scott0bsOLD  9877  infxpenc2  10018  kmlem3  10148  ackbij1lem2  10215  compsscnv  10366  fin1a2lem12  10406  mulerpqlem  10951  1lt2nq  10969  axi2m1  11155  2p2e4  12386  numsuc  12737  numsucc  12768  decmul10add  12797  5p5e10  12799  6p4e10  12800  7p3e10  12803  xnegmnf  13248  pnfaddmnf  13268  fz12pr  13622  fz0tp  13669  fz0to3un2pr  13670  fz0to4untppr  13671  fz0to5un2tp  13672  fzo13pr  13791  fzo0to2pr  13792  fz01pr  13793  fzo0to3tp  13794  fzo0to42pr  13795  fzo1to4tp  13796  fldiv4p1lem1div2  13882  sq4e2t8  14249  i4  14254  crreczi  14278  fac1  14327  fac3  14330  hashkf  14382  hashinf  14385  dmhashres  14391  hashun3  14434  dmtrclfv  15075  abs0  15356  absi  15357  trirecip  15936  geoihalfsum  15955  esum  16152  tan0  16225  coshval  16229  ef01bndlem  16258  3dvds  16407  3dvdsdec  16408  3dvds2dec  16409  sadc0  16530  3lcm2e6woprm  16691  6lcm4e12  16692  lcmf0  16710  prmo0  17114  prmo3  17119  gcdmodi  17152  karatsuba  17161  43prm  17200  139prm  17202  631prm  17205  1259lem1  17209  1259lem2  17210  1259lem3  17211  1259lem4  17212  1259lem5  17213  2503lem1  17215  2503lem2  17216  2503lem3  17217  4001lem1  17219  4001lem2  17220  4001lem3  17221  4001lem4  17222  setsfun  17249  setsfun0  17250  ndxarg  17274  chnccat  18700  ex-chn2  18712  pmtrsn  19613  psgnprfval1  19616  sylow2a  19713  ablfac1eu  20169  sralem  21327  pzriprng1ALT  21676  opsrtoslem2  22237  ply1plusgfvi  22431  pf1rcl  22539  restcld  23359  neitr  23367  txbasval  23794  txindis  23822  cnmpt1st  23856  cnmpt2nd  23857  ufildr  24119  restmetu  24758  cphipval2  25431  reust  25571  ehl0base  25606  ismbl  25716  mbfimaopnlem  25845  itg10  25878  itg2cnlem2  25952  itgz  25971  dvmptid  26147  cos2pi  26672  tan4thpi  26710  tan4thpiOLD  26711  sincos6thpi  26712  pige3ALT  26716  dfrelog  26761  logm1  26785  dvlog  26847  efopnlem2  26853  cxpexp  26864  root1id  26950  sqrt2cxp2logb9e3  26995  ang180lem2  27006  1cubrlem  27037  quart1  27052  atandm2  27073  efiasin  27084  asinsinlem  27087  asinsin  27088  asin1  27090  acos1  27091  atancj  27106  atanlogsublem  27111  efiatan2  27113  2efiatan  27114  tanatan  27115  dvatan  27131  log2cnv  27140  log2ublem2  27143  log2ublem3  27144  birthday  27150  cht1  27360  chp1  27362  ppi1i  27363  ppi2i  27364  cht2  27367  cht3  27368  bclbnd  27475  bposlem8  27486  2lgslem3c  27593  2lgslem3d  27594  noetasuplem2  27929  noetasuplem3  27930  noetasuplem4  27931  noetainflem4  27935  bday0  28035  old0  28063  new0  28088  left1s  28119  right1s  28120  ltslpss  28132  leslss  28133  mulsproplem13  28352  mulsproplem14  28353  precsexlem1  28431  precsexlem2  28432  oniso  28495  bdayn0sf1o  28594  ax5seglem7  29316  axlowdimlem8  29330  axlowdimlem11  29333  vtxvalsnop  29422  iedgvalsnop  29423  umgrislfupgrlem  29503  usgrexmpledg  29646  usgredgffibi  29708  vdegp1bi  29921  edginwlk  30018  uhgrwkspthlem2  30143  clwwlkvbij  30507  wlk2v2elem2  30554  frgrwopreglem3  30712  ex-dif  30821  ex-xp  30834  ex-rn  30838  ex-lcm  30856  ex-prmo  30857  ip0i  31224  ip1ilem  31225  ipdirilem  31228  ipasslem10  31238  hvnegdii  31461  hvaddcani  31464  hvsubaddi  31465  hisubcomi  31503  normlem0  31508  normlem3  31511  normlem9  31517  bcseqi  31519  norm0  31527  norm-ii-i  31536  norm3difi  31546  normpari  31553  normpar2i  31555  polid2i  31556  shs0i  31848  chj0i  31854  pjsslem  32078  ho0subi  32194  hoaddsubi  32220  hosd1i  32221  hopncani  32223  nmop0  32385  nmfn0  32386  lnopunilem1  32409  lnophmlem2  32416  opsqrlem2  32540  pjclem1  32594  atabsi  32800  dmdbr6ati  32822  inin  32909  iuninc  32952  gtiso  33093  f1od2  33110  fpwrelmapffs  33125  fzodif1  33183  nn0split01  33208  dfdec100  33220  dp20u  33243  dp3mul10  33263  dpmul1000  33264  dpexpp1  33273  dpadd2  33275  dpmul  33278  dpmul4  33279  1mhdrd  33281  cycpmrn  33503  tocyccntz  33504  cos9thpiminplylem4  34215  cos9thpiminplylem5  34216  lmat22det  34252  ordtcnvNEW  34350  ordtrest2NEW  34353  zlmtset  34393  qqhucn  34422  esumnul  34478  mbfmcst  34690  carsggect  34749  eulerpartgbij  34803  eulerpartlemn  34812  fib0  34830  fib1  34831  fib2  34833  fib3  34834  fib4  34835  fib5  34836  fib6  34837  0rrv  34882  coinflipprob  34911  ballotlem2  34920  ballotth  34969  signsvf0  35008  itgexpif  35034  hgt750lem  35079  hgt750lem2  35080  bnj1416  35468  r11  35521  r12  35522  derang0  35674  subfac0  35682  subfac1  35683  satfv1  35868  fmla  35886  fmla0  35887  fmla0xp  35888  fmla1  35892  mthmpps  36087  problem2  36171  quad3  36175  dfrdg2  36298  pprodcnveq  36386  dffv5  36427  dfsuccf2  36446  fullfunfv  36452  ellines  36657  rankeq1o  36676  onint1  36993  bj-xpimasn  37624  bj-pr11val  37674  bj-pr21val  37682  bj-pr22val  37688  bj-nuliotaALT  37727  bj-dfmpoa  37793  bj-opabco  37865  icorempo  38030  finxpreclem4  38073  finxp2o  38078  finxp3o  38079  matunitlindf  38302  poimirlem5  38309  poimirlem22  38326  poimirlem26  38330  poimirlem30  38334  ismblfin  38345  dvtan  38354  asindmre  38387  dvasin  38388  dvacos  38389  areacirclem5  38396  heiborlem6  38500  dmcnvep  39070  dmxrncnvep  39071  dmcnvepres  39072  dmxrnuncnvepres  39074  xrnres4  39110  dfadjliftmap2  39139  blockadjliftmap  39140  dfblockliftmap2  39143  dfsucmap3  39145  dfsuccl2  39152  dfcoels  39202  coss0  39251  refsymrels2  39331  dfeqvrels2  39354  refrelsredund4  39398  hdmap1cbv  42609  lcm4un  42816  lcm5un  42817  lcm6un  42818  lcm7un  42819  lcm8un  42820  3lexlogpow5ineq1  42854  5bc2eq10  42942  imaopab  43035  decpmul  43082  cxpi11d  43137  tan3rdpi  43146  sin2t3rdpi  43147  cos2t3rdpi  43148  readvrec2  43155  remul02  43199  fltnltalem  43427  sum9cubes  43437  diophrw  43523  dnwech  43808  lmhmlnmsplit  43847  fgraphopab  43963  arearect  43975  areaquad  43976  oaomoencom  44077  dmnonrel  44349  imanonrel  44352  cononrel1  44353  cononrel2  44354  rclexi  44374  rtrclex  44376  dfrtrcl5  44388  sqrtcval  44400  resqrtvalex  44404  imsqrtvalex  44405  cnvtrrel  44429  dfrcl2  44433  dfrcl4  44435  iunrelexp0  44461  comptiunov2i  44465  relexpaddss  44477  brtrclfv2  44486  trclfvdecomr  44487  corcltrcl  44498  cotrclrcl  44501  fsovcnvlem  44772  neicvgnvo  44874  mnuprdlem1  45015  hashnzfz  45063  lhe4.4ex1a  45072  tgqioo2  46296  sumnnodd  46379  limsup0  46441  limsup10ex  46520  liminf10ex  46521  cosnegpi  46614  itgsin0pilem1  46697  stoweidlem13  46760  wallispilem4  46815  wallispi2lem1  46818  wallispi2lem2  46819  stirlinglem3  46823  dirkertrigeqlem1  46845  fourierdlem56  46909  fourierdlem57  46910  fourierdlem58  46911  fourierdlem62  46915  fourierdlem103  46956  fourierdlem104  46957  fourierdlem112  46965  sqwvfoura  46975  fouriersw  46978  etransclem23  47004  etransclem36  47017  etransclem38  47019  carageniuncllem1  47268  0ome  47276  ovn02  47315  smflimlem4  47521  smflim  47524  smflim2  47553  smflimsup  47575  smfliminf  47578  nthrucw  47640  cos5t  47649  goldratmolem2  47656  fmtno0  48325  fmtno1  48326  fmtno2  48335  fmtno3  48336  fmtno4  48337  fmtno5lem4  48341  139prmALT  48381  31prm  48382  5tcu2e40  48400  3exp4mod41  48401  41prothprmlem2  48403  41prothprm  48404  ppivalnn4  48412  nnsum3primesgbe  48590  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  bgoldbtbndlem1  48603  tgoldbachlt  48614  isuspgrim0lem  48691  isubgr3stgrlem4  48767  isubgr3stgrlem6  48769  isubgr3stgrlem7  48770  usgrexmpl1vtx  48821  usgrexmpl1edg  48822  usgrexmpl2vtx  48826  usgrexmpl2edg  48827  gpg5gricstgr3  48888  gpgprismgr4cycllem7  48899  cznrnglem  49057  2t6m3t4e0  49161  zlmodzxzldeplem3  49315  ackval0  49493  ackval1  49494  ackval2  49495  ackval3  49496  ackval40  49506  ackval42  49509  ackval50  49511  disjdifb  49621  dftpos6  49686  tposresg  49689  tposrescnv  49690  tposres3  49692  tposid  49696  iscnrm3rlem1  49751  dfswapf2  50072  setc1onsubc  50413  sec0  50571  crosspdotsumi  50679  crossp3i  50682