Theorem 3eqtri 2788

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

Syntax hints:   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  csbid  3863  csbconstg  3869  csbie  3885  un23  4124  in32  4179  dfnul4  4285  unvdif  4426  undif2  4428  undifabs  4429  difun2  4432  difdifdir  4442  dfif4  4493  dfif5  4494  tpidm23  4713  dfopif  4825  dfiunv2  4988  symdif0  5039  symdifv  5040  symdifid  5041  unidif0  5313  unidif0OLD  5314  uniop  5481  xpun  5717  dfrn2  5860  dfdmf  5868  dfrnf  5922  res0  5965  resres  5974  xpssres  6000  dfima2  6047  imai  6059  ima0  6062  imaundir  6131  xpima  6163  cnvrescnv  6177  dmresv  6182  rescnvcnv  6186  dmtpop  6200  rnsnopg  6203  resdmres  6214  resdifdi  6218  dmmpt  6222  dmco  6237  co01  6244  suc0  6418  iunsuc  6428  fresaun  6730  dffv4  6859  f1ossf1o  7105  fpr  7132  mpo0  7476  dmoprab  7494  rnoprab  7496  elrnmpores  7529  ov6g  7555  1st0  7971  2nd0  7972  dfmpo  8075  curry1  8077  curry2  8080  fpar  8089  dftpos2  8217  tposoprab  8236  tposmpo  8237  fvmpocurryd  8245  frrlem14  8274  dfrecs3  8337  tfrlem8  8349  seqomlem3  8417  df2o3  8439  nlim2  8453  omxpenlem  9044  dfsdom2  9066  pwfir  9255  marypha2lem2  9376  sup00  9405  epinid0  9547  scottexs  9839  scott0s  9840  infxpenc2  9972  kmlem3  10103  ackbij1lem2  10170  compsscnv  10322  fin1a2lem12  10362  mulerpqlem  10907  1lt2nq  10925  axi2m1  11111  2p2e4  12346  numsuc  12696  numsucc  12727  decmul10add  12756  5p5e10  12758  6p4e10  12759  7p3e10  12762  xnegmnf  13207  pnfaddmnf  13227  fz12pr  13580  fz0tp  13627  fz0to3un2pr  13628  fz0to4untppr  13629  fz0to5un2tp  13630  fzo13pr  13749  fzo0to2pr  13750  fz01pr  13751  fzo0to3tp  13752  fzo0to42pr  13753  fzo1to4tp  13754  fldiv4p1lem1div2  13839  sq4e2t8  14206  i4  14211  crreczi  14235  fac1  14284  fac3  14287  hashkf  14339  hashinf  14342  dmhashres  14348  hashun3  14391  dmtrclfv  15025  abs0  15303  absi  15304  trirecip  15884  geoihalfsum  15903  esum  16101  tan0  16174  coshval  16178  ef01bndlem  16207  3dvds  16356  3dvdsdec  16357  3dvds2dec  16358  sadc0  16479  3lcm2e6woprm  16640  6lcm4e12  16641  lcmf0  16659  prmo0  17063  gcdmodi  17101  karatsuba  17110  43prm  17149  139prm  17151  631prm  17154  1259lem1  17158  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  2503lem1  17164  2503lem2  17165  2503lem3  17166  4001lem1  17168  4001lem2  17169  4001lem3  17170  4001lem4  17171  setsfun  17198  setsfun0  17199  ndxarg  17223  chnccat  18649  ex-chn2  18661  pmtrsn  19550  psgnprfval1  19553  sylow2a  19650  ablfac1eu  20106  sralem  21231  pzriprng1ALT  21536  opsrtoslem2  22097  ply1plusgfvi  22291  pf1rcl  22400  restcld  23220  neitr  23228  txbasval  23654  txindis  23682  cnmpt1st  23716  cnmpt2nd  23717  ufildr  23979  restmetu  24618  cphipval2  25291  reust  25431  ehl0base  25466  ismbl  25576  mbfimaopnlem  25705  itg10  25738  itg2cnlem2  25812  itgz  25831  dvmptid  26007  cos2pi  26529  tan4thpi  26567  tan4thpiOLD  26568  sincos6thpi  26569  pige3ALT  26573  dfrelog  26618  logm1  26642  dvlog  26704  efopnlem2  26710  cxpexp  26721  root1id  26807  sqrt2cxp2logb9e3  26852  ang180lem2  26863  1cubrlem  26894  quart1  26909  atandm2  26930  efiasin  26941  asinsinlem  26944  asinsin  26945  asin1  26947  acos1  26948  atancj  26963  atanlogsublem  26968  efiatan2  26970  2efiatan  26971  tanatan  26972  dvatan  26988  log2cnv  26997  log2ublem2  27000  log2ublem3  27001  birthday  27007  basellem8  27140  cht1  27217  chp1  27219  ppi1i  27220  ppi2i  27221  cht2  27224  cht3  27225  bclbnd  27332  bposlem8  27343  2lgslem3c  27450  2lgslem3d  27451  noetasuplem2  27786  noetasuplem3  27787  noetasuplem4  27788  noetainflem4  27792  bday0  27892  old0  27920  new0  27945  left1s  27976  right1s  27977  ltslpss  27989  leslss  27990  mulsproplem13  28209  mulsproplem14  28210  precsexlem1  28288  precsexlem2  28289  oniso  28352  bdayn0sf1o  28451  ax5seglem7  29093  axlowdimlem8  29107  axlowdimlem11  29110  vtxvalsnop  29199  iedgvalsnop  29200  umgrislfupgrlem  29280  usgrexmpledg  29420  usgredgffibi  29482  vdegp1bi  29695  edginwlk  29792  uhgrwkspthlem2  29911  clwwlkvbij  30272  wlk2v2elem2  30315  frgrwopreglem3  30473  ex-dif  30582  ex-xp  30595  ex-rn  30599  ex-lcm  30617  ex-prmo  30618  ip0i  30985  ip1ilem  30986  ipdirilem  30989  ipasslem10  30999  hvnegdii  31222  hvaddcani  31225  hvsubaddi  31226  hisubcomi  31264  normlem0  31269  normlem3  31272  normlem9  31278  bcseqi  31280  norm0  31288  norm-ii-i  31297  norm3difi  31307  normpari  31314  normpar2i  31316  polid2i  31317  shs0i  31609  chj0i  31615  pjsslem  31839  ho0subi  31955  hoaddsubi  31981  hosd1i  31982  hopncani  31984  nmop0  32146  nmfn0  32147  lnopunilem1  32170  lnophmlem2  32177  opsqrlem2  32301  pjclem1  32355  atabsi  32561  dmdbr6ati  32583  inin  32675  iuninc  32720  gtiso  32864  f1od2  32882  fpwrelmapffs  32897  fzodif1  32955  nn0split01  32981  dfdec100  32993  dp20u  33016  dp3mul10  33036  dpmul1000  33037  dpexpp1  33046  dpadd2  33048  dpmul  33051  dpmul4  33052  1mhdrd  33054  cycpmrn  33284  tocyccntz  33285  cos9thpiminplylem4  34043  cos9thpiminplylem5  34044  lmat22det  34080  ordtcnvNEW  34178  ordtrest2NEW  34181  zlmtset  34221  qqhucn  34250  esumnul  34306  mbfmcst  34517  carsggect  34576  eulerpartgbij  34630  eulerpartlemn  34639  fib0  34657  fib1  34658  fib2  34660  fib3  34661  fib4  34662  fib5  34663  fib6  34664  0rrv  34709  coinflipprob  34738  ballotlem2  34747  ballotth  34796  signsvf0  34835  itgexpif  34861  hgt750lem  34906  hgt750lem2  34907  bnj1416  35295  r11  35351  r12  35352  derang0  35480  subfac0  35488  subfac1  35489  satfv1  35674  fmla  35692  fmla0  35693  fmla0xp  35694  fmla1  35698  mthmpps  35893  problem2  35977  quad3  35981  dfrdg2  36104  pprodcnveq  36192  dffv5  36233  dfsuccf2  36252  fullfunfv  36258  ellines  36463  rankeq1o  36482  onint1  36770  bj-xpimasn  37401  bj-pr11val  37451  bj-pr21val  37459  bj-pr22val  37465  bj-nuliotaALT  37504  bj-dfmpoa  37569  bj-opabco  37641  icorempo  37806  finxpreclem4  37849  finxp2o  37854  finxp3o  37855  matunitlindf  38078  poimirlem5  38085  poimirlem22  38102  poimirlem26  38106  poimirlem30  38110  ismblfin  38121  dvtan  38130  asindmre  38163  dvasin  38164  dvacos  38165  areacirclem5  38172  heiborlem6  38276  dmcnvep  38848  dmxrncnvep  38849  dmcnvepres  38850  dmxrnuncnvepres  38852  xrnres4  38888  dfadjliftmap2  38917  blockadjliftmap  38918  dfblockliftmap2  38921  dfsucmap3  38923  dfsuccl2  38930  dfcoels  38980  coss0  39029  refsymrels2  39109  dfeqvrels2  39132  refrelsredund4  39176  hdmap1cbv  42387  lcm4un  42594  lcm5un  42595  lcm6un  42596  lcm7un  42597  lcm8un  42598  3lexlogpow5ineq1  42632  5bc2eq10  42720  imaopab  42811  decpmul  42858  cxpi11d  42913  tan3rdpi  42922  sin2t3rdpi  42923  cos2t3rdpi  42924  readvrec2  42931  remul02  42975  fltnltalem  43205  sum9cubes  43215  diophrw  43301  dnwech  43586  lmhmlnmsplit  43625  fgraphopab  43741  arearect  43753  areaquad  43754  oaomoencom  43855  dmnonrel  44127  imanonrel  44130  cononrel1  44131  cononrel2  44132  rclexi  44152  rtrclex  44154  dfrtrcl5  44166  sqrtcval  44178  resqrtvalex  44182  imsqrtvalex  44183  cnvtrrel  44207  dfrcl2  44211  dfrcl4  44213  iunrelexp0  44239  comptiunov2i  44243  relexpaddss  44255  brtrclfv2  44264  trclfvdecomr  44265  corcltrcl  44276  cotrclrcl  44279  fsovcnvlem  44550  neicvgnvo  44652  scottabf  44777  mnuprdlem1  44809  hashnzfz  44857  lhe4.4ex1a  44866  tgqioo2  46084  sumnnodd  46167  limsup0  46229  limsup10ex  46308  liminf10ex  46309  cosnegpi  46402  itgsin0pilem1  46485  stoweidlem13  46548  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  stirlinglem3  46611  dirkertrigeqlem1  46633  fourierdlem56  46697  fourierdlem57  46698  fourierdlem58  46699  fourierdlem62  46703  fourierdlem103  46744  fourierdlem104  46745  fourierdlem112  46753  sqwvfoura  46763  fouriersw  46766  etransclem23  46792  etransclem36  46805  etransclem38  46807  carageniuncllem1  47056  0ome  47064  ovn02  47103  smflimlem4  47309  smflim  47312  smflim2  47341  smflimsup  47363  smfliminf  47366  cos5t  47434  goldratmolem2  47441  fmtno0  48110  fmtno1  48111  fmtno2  48120  fmtno3  48121  fmtno4  48122  fmtno5lem4  48126  139prmALT  48166  31prm  48167  5tcu2e40  48185  3exp4mod41  48186  41prothprmlem2  48188  41prothprm  48189  ppivalnn4  48197  nnsum3primesgbe  48375  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  nnsum4primeseven  48383  nnsum4primesevenALTV  48384  bgoldbtbndlem1  48388  tgoldbachlt  48399  isuspgrim0lem  48476  isubgr3stgrlem4  48552  isubgr3stgrlem6  48554  isubgr3stgrlem7  48555  usgrexmpl1vtx  48606  usgrexmpl1edg  48607  usgrexmpl2vtx  48611  usgrexmpl2edg  48612  gpg5gricstgr3  48673  gpgprismgr4cycllem7  48684  cznrnglem  48842  2t6m3t4e0  48931  zlmodzxzldeplem3  49085  ackval0  49263  ackval1  49264  ackval2  49265  ackval3  49266  ackval40  49276  ackval42  49279  ackval50  49281  disjdifb  49392  dftpos6  49457  tposresg  49460  tposrescnv  49461  tposres3  49463  tposid  49467  iscnrm3rlem1  49522  dfswapf2  49843  setc1onsubc  50184  sec0  50342