Theorem 3eqtri 2796

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  csbid  3874  csbconstg  3880  csbie  3896  un23  4135  in32  4190  dfnul4  4296  unvdif  4438  undif2  4440  undifabs  4441  difun2  4444  difdifdir  4454  dfif4  4505  dfif5  4506  tpidm23  4725  dfopif  4836  dfiunv2  4999  symdif0  5052  symdifv  5053  symdifid  5054  unidif0  5328  unidif0OLD  5329  uniop  5496  xpun  5733  dfrn2  5876  dfdmf  5884  dfrnf  5938  res0  5980  resres  5989  xpssres  6015  dfima2  6062  imai  6074  ima0  6077  imaundir  6146  xpima  6179  cnvrescnv  6193  dmresv  6198  rescnvcnv  6202  dmtpop  6216  rnsnopg  6219  resdmres  6230  resdifdi  6234  dmmpt  6238  dmco  6253  co01  6260  suc0  6435  iunsuc  6445  fresaun  6747  dffv4  6876  f1ossf1o  7122  fpr  7149  mpo0  7493  dmoprab  7511  rnoprab  7513  elrnmpores  7546  ov6g  7572  1st0  7988  2nd0  7989  dfmpo  8093  curry1  8095  curry2  8098  fpar  8107  dftpos2  8235  tposoprab  8254  tposmpo  8255  fvmpocurryd  8263  frrlem14  8292  dfrecs3  8355  tfrlem8  8367  seqomlem3  8435  df2o3  8457  nlim2  8471  omxpenlem  9062  dfsdom2  9084  pwfir  9272  marypha2lem2  9392  sup00  9421  epinid0  9563  scottexs  9857  scott0s  9858  scottabf  9862  infxpenc2  10002  kmlem3  10132  ackbij1lem2  10199  compsscnv  10351  fin1a2lem12  10391  mulerpqlem  10936  1lt2nq  10954  axi2m1  11140  2p2e4  12371  numsuc  12721  numsucc  12752  decmul10add  12781  5p5e10  12783  6p4e10  12784  7p3e10  12787  xnegmnf  13232  pnfaddmnf  13252  fz12pr  13605  fz0tp  13652  fz0to3un2pr  13653  fz0to4untppr  13654  fz0to5un2tp  13655  fzo13pr  13774  fzo0to2pr  13775  fz01pr  13776  fzo0to3tp  13777  fzo0to42pr  13778  fzo1to4tp  13779  fldiv4p1lem1div2  13864  sq4e2t8  14231  i4  14236  crreczi  14260  fac1  14309  fac3  14312  hashkf  14364  hashinf  14367  dmhashres  14373  hashun3  14416  dmtrclfv  15051  abs0  15332  absi  15333  trirecip  15913  geoihalfsum  15932  esum  16130  tan0  16203  coshval  16207  ef01bndlem  16236  3dvds  16385  3dvdsdec  16386  3dvds2dec  16387  sadc0  16508  3lcm2e6woprm  16669  6lcm4e12  16670  lcmf0  16688  prmo0  17092  gcdmodi  17130  karatsuba  17139  43prm  17178  139prm  17180  631prm  17183  1259lem1  17187  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  2503lem1  17193  2503lem2  17194  2503lem3  17195  4001lem1  17197  4001lem2  17198  4001lem3  17199  4001lem4  17200  setsfun  17227  setsfun0  17228  ndxarg  17252  chnccat  18678  ex-chn2  18690  pmtrsn  19585  psgnprfval1  19588  sylow2a  19685  ablfac1eu  20141  sralem  21271  pzriprng1ALT  21611  opsrtoslem2  22172  ply1plusgfvi  22366  pf1rcl  22474  restcld  23294  neitr  23302  txbasval  23728  txindis  23756  cnmpt1st  23790  cnmpt2nd  23791  ufildr  24053  restmetu  24692  cphipval2  25365  reust  25505  ehl0base  25540  ismbl  25650  mbfimaopnlem  25779  itg10  25812  itg2cnlem2  25886  itgz  25905  dvmptid  26081  cos2pi  26603  tan4thpi  26641  tan4thpiOLD  26642  sincos6thpi  26643  pige3ALT  26647  dfrelog  26692  logm1  26716  dvlog  26778  efopnlem2  26784  cxpexp  26795  root1id  26881  sqrt2cxp2logb9e3  26926  ang180lem2  26937  1cubrlem  26968  quart1  26983  atandm2  27004  efiasin  27015  asinsinlem  27018  asinsin  27019  asin1  27021  acos1  27022  atancj  27037  atanlogsublem  27042  efiatan2  27044  2efiatan  27045  tanatan  27046  dvatan  27062  log2cnv  27071  log2ublem2  27074  log2ublem3  27075  birthday  27081  basellem8  27214  cht1  27291  chp1  27293  ppi1i  27294  ppi2i  27295  cht2  27298  cht3  27299  bclbnd  27406  bposlem8  27417  2lgslem3c  27524  2lgslem3d  27525  noetasuplem2  27860  noetasuplem3  27861  noetasuplem4  27862  noetainflem4  27866  bday0  27966  old0  27994  new0  28019  left1s  28050  right1s  28051  ltslpss  28063  leslss  28064  mulsproplem13  28283  mulsproplem14  28284  precsexlem1  28362  precsexlem2  28363  oniso  28426  bdayn0sf1o  28525  ax5seglem7  29222  axlowdimlem8  29236  axlowdimlem11  29239  vtxvalsnop  29328  iedgvalsnop  29329  umgrislfupgrlem  29409  usgrexmpledg  29549  usgredgffibi  29611  vdegp1bi  29824  edginwlk  29921  uhgrwkspthlem2  30040  clwwlkvbij  30401  wlk2v2elem2  30444  frgrwopreglem3  30602  ex-dif  30711  ex-xp  30724  ex-rn  30728  ex-lcm  30746  ex-prmo  30747  ip0i  31114  ip1ilem  31115  ipdirilem  31118  ipasslem10  31128  hvnegdii  31351  hvaddcani  31354  hvsubaddi  31355  hisubcomi  31393  normlem0  31398  normlem3  31401  normlem9  31407  bcseqi  31409  norm0  31417  norm-ii-i  31426  norm3difi  31436  normpari  31443  normpar2i  31445  polid2i  31446  shs0i  31738  chj0i  31744  pjsslem  31968  ho0subi  32084  hoaddsubi  32110  hosd1i  32111  hopncani  32113  nmop0  32275  nmfn0  32276  lnopunilem1  32299  lnophmlem2  32306  opsqrlem2  32430  pjclem1  32484  atabsi  32690  dmdbr6ati  32712  inin  32799  iuninc  32842  gtiso  32983  f1od2  33001  fpwrelmapffs  33016  fzodif1  33074  nn0split01  33099  dfdec100  33111  dp20u  33134  dp3mul10  33154  dpmul1000  33155  dpexpp1  33164  dpadd2  33166  dpmul  33169  dpmul4  33170  1mhdrd  33172  cycpmrn  33400  tocyccntz  33401  cos9thpiminplylem4  34116  cos9thpiminplylem5  34117  lmat22det  34153  ordtcnvNEW  34251  ordtrest2NEW  34254  zlmtset  34294  qqhucn  34323  esumnul  34379  mbfmcst  34590  carsggect  34649  eulerpartgbij  34703  eulerpartlemn  34712  fib0  34730  fib1  34731  fib2  34733  fib3  34734  fib4  34735  fib5  34736  fib6  34737  0rrv  34782  coinflipprob  34811  ballotlem2  34820  ballotth  34869  signsvf0  34908  itgexpif  34934  hgt750lem  34979  hgt750lem2  34980  bnj1416  35368  r11  35426  r12  35427  derang0  35556  subfac0  35564  subfac1  35565  satfv1  35750  fmla  35768  fmla0  35769  fmla0xp  35770  fmla1  35774  mthmpps  35969  problem2  36053  quad3  36057  dfrdg2  36180  pprodcnveq  36268  dffv5  36309  dfsuccf2  36328  fullfunfv  36334  ellines  36539  rankeq1o  36558  onint1  36845  bj-xpimasn  37475  bj-pr11val  37525  bj-pr21val  37533  bj-pr22val  37539  bj-nuliotaALT  37578  bj-dfmpoa  37643  bj-opabco  37715  icorempo  37880  finxpreclem4  37923  finxp2o  37928  finxp3o  37929  matunitlindf  38152  poimirlem5  38159  poimirlem22  38176  poimirlem26  38180  poimirlem30  38184  ismblfin  38195  dvtan  38204  asindmre  38237  dvasin  38238  dvacos  38239  areacirclem5  38246  heiborlem6  38350  dmcnvep  38922  dmxrncnvep  38923  dmcnvepres  38924  dmxrnuncnvepres  38926  xrnres4  38962  dfadjliftmap2  38991  blockadjliftmap  38992  dfblockliftmap2  38995  dfsucmap3  38997  dfsuccl2  39004  dfcoels  39054  coss0  39103  refsymrels2  39183  dfeqvrels2  39206  refrelsredund4  39250  hdmap1cbv  42461  lcm4un  42668  lcm5un  42669  lcm6un  42670  lcm7un  42671  lcm8un  42672  3lexlogpow5ineq1  42706  5bc2eq10  42794  imaopab  42885  decpmul  42932  cxpi11d  42987  tan3rdpi  42996  sin2t3rdpi  42997  cos2t3rdpi  42998  readvrec2  43005  remul02  43049  fltnltalem  43279  sum9cubes  43289  diophrw  43375  dnwech  43660  lmhmlnmsplit  43699  fgraphopab  43815  arearect  43827  areaquad  43828  oaomoencom  43929  dmnonrel  44201  imanonrel  44204  cononrel1  44205  cononrel2  44206  rclexi  44226  rtrclex  44228  dfrtrcl5  44240  sqrtcval  44252  resqrtvalex  44256  imsqrtvalex  44257  cnvtrrel  44281  dfrcl2  44285  dfrcl4  44287  iunrelexp0  44313  comptiunov2i  44317  relexpaddss  44329  brtrclfv2  44338  trclfvdecomr  44339  corcltrcl  44350  cotrclrcl  44353  fsovcnvlem  44624  neicvgnvo  44726  mnuprdlem1  44867  hashnzfz  44915  lhe4.4ex1a  44924  tgqioo2  46148  sumnnodd  46231  limsup0  46293  limsup10ex  46372  liminf10ex  46373  cosnegpi  46466  itgsin0pilem1  46549  stoweidlem13  46612  wallispilem4  46667  wallispi2lem1  46670  wallispi2lem2  46671  stirlinglem3  46675  dirkertrigeqlem1  46697  fourierdlem56  46761  fourierdlem57  46762  fourierdlem58  46763  fourierdlem62  46767  fourierdlem103  46808  fourierdlem104  46809  fourierdlem112  46817  sqwvfoura  46827  fouriersw  46830  etransclem23  46856  etransclem36  46869  etransclem38  46871  carageniuncllem1  47120  0ome  47128  ovn02  47167  smflimlem4  47373  smflim  47376  smflim2  47405  smflimsup  47427  smfliminf  47430  cos5t  47498  goldratmolem2  47505  fmtno0  48174  fmtno1  48175  fmtno2  48184  fmtno3  48185  fmtno4  48186  fmtno5lem4  48190  139prmALT  48230  31prm  48231  5tcu2e40  48249  3exp4mod41  48250  41prothprmlem2  48252  41prothprm  48253  ppivalnn4  48261  nnsum3primesgbe  48439  nnsum4primesodd  48443  nnsum4primesoddALTV  48444  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  bgoldbtbndlem1  48452  tgoldbachlt  48463  isuspgrim0lem  48540  isubgr3stgrlem4  48616  isubgr3stgrlem6  48618  isubgr3stgrlem7  48619  usgrexmpl1vtx  48670  usgrexmpl1edg  48671  usgrexmpl2vtx  48675  usgrexmpl2edg  48676  gpg5gricstgr3  48737  gpgprismgr4cycllem7  48748  cznrnglem  48906  2t6m3t4e0  49006  zlmodzxzldeplem3  49160  ackval0  49338  ackval1  49339  ackval2  49340  ackval3  49341  ackval40  49351  ackval42  49354  ackval50  49356  disjdifb  49466  dftpos6  49531  tposresg  49534  tposrescnv  49535  tposres3  49537  tposid  49541  iscnrm3rlem1  49596  dfswapf2  49917  setc1onsubc  50258  sec0  50416