Theorem 3eqtri 2763

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  csbid  3862  csbconstg  3868  csbie  3884  un23  4126  in32  4182  dfnul4  4287  unvdif  4427  undif2  4429  undifabs  4430  difun2  4433  difdifdir  4444  dfif4  4495  dfif5  4496  tpidm23  4714  dfopif  4826  dfiunv2  4989  symdif0  5040  symdifid  5042  unidif0  5305  uniop  5463  xpun  5698  dfrn2  5837  dfdmf  5845  dfrnf  5899  res0  5942  resres  5951  xpssres  5977  dfima2  6021  imai  6033  ima0  6036  imaundir  6108  xpima  6140  cnvrescnv  6153  dmresv  6158  rescnvcnv  6162  dmtpop  6176  rnsnopg  6179  resdmres  6190  resdifdi  6194  dmmpt  6198  dmco  6213  co01  6220  suc0  6394  iunsuc  6404  fresaun  6705  dffv4  6831  f1ossf1o  7073  fpr  7099  mpo0  7443  dmoprab  7461  rnoprab  7463  elrnmpores  7496  ov6g  7522  1st0  7939  2nd0  7940  dfmpo  8044  curry1  8046  curry2  8049  fpar  8058  dftpos2  8185  tposoprab  8204  tposmpo  8205  fvmpocurryd  8213  frrlem14  8241  dfrecs3  8304  tfrlem8  8315  seqomlem3  8383  df2o3  8405  nlim2  8417  omxpenlem  9006  dfsdom2  9028  pwfir  9217  marypha2lem2  9339  sup00  9368  epinid0  9508  scottexs  9799  scott0s  9800  infxpenc2  9932  kmlem3  10063  ackbij1lem2  10130  compsscnv  10281  fin1a2lem12  10321  mulerpqlem  10866  1lt2nq  10884  axi2m1  11070  2p2e4  12275  numsuc  12621  numsucc  12647  decmul10add  12676  5p5e10  12678  6p4e10  12679  7p3e10  12682  xnegmnf  13125  pnfaddmnf  13145  fz12pr  13497  fz0tp  13544  fz0to3un2pr  13545  fz0to4untppr  13546  fz0to5un2tp  13547  fzo13pr  13665  fzo0to2pr  13666  fz01pr  13667  fzo0to3tp  13668  fzo0to42pr  13669  fzo1to4tp  13670  fldiv4p1lem1div2  13755  sq4e2t8  14122  i4  14127  crreczi  14151  fac1  14200  fac3  14203  hashkf  14255  hashinf  14258  dmhashres  14264  hashun3  14307  dmtrclfv  14941  abs0  15208  absi  15209  trirecip  15786  geoihalfsum  15805  esum  16003  tan0  16076  coshval  16080  ef01bndlem  16109  3dvds  16258  3dvdsdec  16259  3dvds2dec  16260  sadc0  16381  3lcm2e6woprm  16542  6lcm4e12  16543  lcmf0  16561  prmo0  16964  gcdmodi  17002  karatsuba  17011  43prm  17049  139prm  17051  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  setsfun  17098  setsfun0  17099  ndxarg  17123  chnccat  18549  ex-chn2  18561  pmtrsn  19448  psgnprfval1  19451  sylow2a  19548  ablfac1eu  20004  sralem  21128  pzriprng1ALT  21451  opsrtoslem2  22011  ply1plusgfvi  22182  pf1rcl  22293  restcld  23116  neitr  23124  txbasval  23550  txindis  23578  cnmpt1st  23612  cnmpt2nd  23613  ufildr  23875  restmetu  24514  cphipval2  25197  reust  25337  ehl0base  25372  ismbl  25483  mbfimaopnlem  25612  itg10  25645  itg2cnlem2  25719  itgz  25738  dvmptid  25917  cos2pi  26441  tan4thpi  26479  tan4thpiOLD  26480  sincos6thpi  26481  pige3ALT  26485  dfrelog  26530  logm1  26554  dvlog  26616  efopnlem2  26622  cxpexp  26633  root1id  26720  sqrt2cxp2logb9e3  26765  ang180lem2  26776  1cubrlem  26807  quart1  26822  atandm2  26843  efiasin  26854  asinsinlem  26857  asinsin  26858  asin1  26860  acos1  26861  atancj  26876  atanlogsublem  26881  efiatan2  26883  2efiatan  26884  tanatan  26885  dvatan  26901  log2cnv  26910  log2ublem2  26913  log2ublem3  26914  birthday  26920  basellem8  27054  cht1  27131  chp1  27133  ppi1i  27134  ppi2i  27135  cht2  27138  cht3  27139  bclbnd  27247  bposlem8  27258  2lgslem3c  27365  2lgslem3d  27366  noetasuplem2  27702  noetasuplem3  27703  noetasuplem4  27704  noetainflem4  27708  bday0  27807  old0  27835  new0  27860  left1s  27891  right1s  27892  ltslpss  27904  leslss  27905  mulsproplem13  28124  mulsproplem14  28125  precsexlem1  28203  precsexlem2  28204  oniso  28267  bdayn0sf1o  28366  ax5seglem7  29008  axlowdimlem8  29022  axlowdimlem11  29025  vtxvalsnop  29114  iedgvalsnop  29115  umgrislfupgrlem  29195  usgrexmpledg  29335  usgredgffibi  29397  vdegp1bi  29611  edginwlk  29708  uhgrwkspthlem2  29827  clwwlkvbij  30188  wlk2v2elem2  30231  frgrwopreglem3  30389  ex-dif  30498  ex-xp  30511  ex-rn  30515  ex-lcm  30533  ex-prmo  30534  ip0i  30900  ip1ilem  30901  ipdirilem  30904  ipasslem10  30914  hvnegdii  31137  hvaddcani  31140  hvsubaddi  31141  hisubcomi  31179  normlem0  31184  normlem3  31187  normlem9  31193  bcseqi  31195  norm0  31203  norm-ii-i  31212  norm3difi  31222  normpari  31229  normpar2i  31231  polid2i  31232  shs0i  31524  chj0i  31530  pjsslem  31754  ho0subi  31870  hoaddsubi  31896  hosd1i  31897  hopncani  31899  nmop0  32061  nmfn0  32062  lnopunilem1  32085  lnophmlem2  32092  opsqrlem2  32216  pjclem1  32270  atabsi  32476  dmdbr6ati  32498  inin  32591  iuninc  32635  gtiso  32780  f1od2  32798  fpwrelmapffs  32813  fzodif1  32872  nn0split01  32898  dfdec100  32911  dp20u  32959  dp3mul10  32979  dpmul1000  32980  dpexpp1  32989  dpadd2  32991  dpmul  32994  dpmul4  32995  1mhdrd  32997  cycpmrn  33225  tocyccntz  33226  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  lmat22det  33979  ordtcnvNEW  34077  ordtrest2NEW  34080  zlmtset  34120  qqhucn  34149  esumnul  34205  mbfmcst  34416  carsggect  34475  eulerpartgbij  34529  eulerpartlemn  34538  fib0  34556  fib1  34557  fib2  34559  fib3  34560  fib4  34561  fib5  34562  fib6  34563  0rrv  34608  coinflipprob  34637  ballotlem2  34646  ballotth  34695  signsvf0  34737  itgexpif  34763  hgt750lem  34808  hgt750lem2  34809  bnj1416  35195  r11  35250  r12  35251  derang0  35363  subfac0  35371  subfac1  35372  satfv1  35557  fmla  35575  fmla0  35576  fmla0xp  35577  fmla1  35581  mthmpps  35776  problem2  35860  quad3  35864  dfrdg2  35987  pprodcnveq  36075  dffv5  36116  dfsuccf2  36135  fullfunfv  36141  ellines  36346  rankeq1o  36365  onint1  36643  bj-xpimasn  37156  bj-pr11val  37206  bj-pr21val  37214  bj-pr22val  37220  bj-nuliotaALT  37259  bj-dfmpoa  37323  bj-opabco  37393  icorempo  37556  finxpreclem4  37599  finxp2o  37604  finxp3o  37605  matunitlindf  37819  poimirlem5  37826  poimirlem22  37843  poimirlem26  37847  poimirlem30  37851  ismblfin  37862  dvtan  37871  asindmre  37904  dvasin  37905  dvacos  37906  areacirclem5  37913  heiborlem6  38017  dmcnvep  38573  dmxrncnvep  38574  dmcnvepres  38575  dmxrnuncnvepres  38577  xrnres4  38613  dfadjliftmap2  38632  blockadjliftmap  38633  dfblockliftmap2  38635  dfsucmap3  38637  dfsuccl2  38644  dfcoels  38693  coss0  38742  refsymrels2  38822  dfeqvrels2  38845  refrelsredund4  38889  hdmap1cbv  42062  lcm4un  42270  lcm5un  42271  lcm6un  42272  lcm7un  42273  lcm8un  42274  3lexlogpow5ineq1  42308  5bc2eq10  42396  imaopab  42487  decpmul  42543  cxpi11d  42598  tan3rdpi  42607  sin2t3rdpi  42608  cos2t3rdpi  42609  readvrec2  42616  remul02  42660  fltnltalem  42905  sum9cubes  42915  diophrw  43001  dnwech  43290  lmhmlnmsplit  43329  fgraphopab  43445  arearect  43457  areaquad  43458  oaomoencom  43559  dmnonrel  43831  imanonrel  43834  cononrel1  43835  cononrel2  43836  rclexi  43856  rtrclex  43858  dfrtrcl5  43870  sqrtcval  43882  resqrtvalex  43886  imsqrtvalex  43887  cnvtrrel  43911  dfrcl2  43915  dfrcl4  43917  iunrelexp0  43943  comptiunov2i  43947  relexpaddss  43959  brtrclfv2  43968  trclfvdecomr  43969  corcltrcl  43980  cotrclrcl  43983  fsovcnvlem  44254  neicvgnvo  44356  scottabf  44481  mnuprdlem1  44513  hashnzfz  44561  lhe4.4ex1a  44570  tgqioo2  45793  sumnnodd  45876  limsup0  45938  limsup10ex  46017  liminf10ex  46018  cosnegpi  46111  itgsin0pilem1  46194  stoweidlem13  46257  wallispilem4  46312  wallispi2lem1  46315  wallispi2lem2  46316  stirlinglem3  46320  dirkertrigeqlem1  46342  fourierdlem56  46406  fourierdlem57  46407  fourierdlem58  46408  fourierdlem62  46412  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  sqwvfoura  46472  fouriersw  46475  etransclem23  46501  etransclem36  46514  etransclem38  46516  carageniuncllem1  46765  0ome  46773  ovn02  46812  smflimlem4  47018  smflim  47021  smflim2  47050  smflimsup  47072  smfliminf  47075  fmtno0  47786  fmtno1  47787  fmtno2  47796  fmtno3  47797  fmtno4  47798  fmtno5lem4  47802  139prmALT  47842  31prm  47843  5tcu2e40  47861  3exp4mod41  47862  41prothprmlem2  47864  41prothprm  47865  nnsum3primesgbe  48038  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbtbndlem1  48051  tgoldbachlt  48062  isuspgrim0lem  48139  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  isubgr3stgrlem7  48218  usgrexmpl1vtx  48269  usgrexmpl1edg  48270  usgrexmpl2vtx  48274  usgrexmpl2edg  48275  gpg5gricstgr3  48336  gpgprismgr4cycllem7  48347  cznrnglem  48505  2t6m3t4e0  48594  zlmodzxzldeplem3  48748  ackval0  48926  ackval1  48927  ackval2  48928  ackval3  48929  ackval40  48939  ackval42  48942  ackval50  48944  disjdifb  49055  dftpos6  49120  tposresg  49123  tposrescnv  49124  tposres3  49126  tposid  49130  iscnrm3rlem1  49185  dfswapf2  49506  setc1onsubc  49847  sec0  50005