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  4441  undif2  4443  undifabs  4444  difun2  4447  difdifdir  4457  dfif4  4508  dfif5  4509  tpidm23  4728  dfopif  4839  dfiunv2  5002  symdif0  5055  symdifv  5056  symdifid  5057  unidif0  5331  unidif0OLD  5332  uniop  5499  xpun  5736  dfrn2  5879  dfdmf  5887  dfrnf  5941  res0  5983  resres  5992  xpssres  6018  dfima2  6065  imai  6077  ima0  6080  imaundir  6149  xpima  6181  cnvrescnv  6195  dmresv  6200  rescnvcnv  6206  dmtpop  6220  rnsnopg  6223  resdmres  6234  resdifdi  6238  dmmpt  6242  dmco  6257  co01  6264  suc0  6439  iunsuc  6449  fresaun  6750  dffv4  6879  f1ossf1o  7125  fpr  7152  mpo0  7496  dmoprab  7514  rnoprab  7516  elrnmpores  7549  ov6g  7575  1st0  7992  2nd0  7993  dfmpo  8097  curry1  8099  curry2  8102  fpar  8111  dftpos2  8239  tposoprab  8258  tposmpo  8259  fvmpocurryd  8267  frrlem14  8296  dfrecs3  8359  tfrlem8  8371  seqomlem3  8439  df2o3  8461  nlim2  8475  omxpenlem  9066  dfsdom2  9088  pwfir  9276  marypha2lem2  9396  sup00  9425  epinid0  9567  scottexs  9861  scott0s  9862  scottabf  9866  infxpenc2  10006  kmlem3  10136  ackbij1lem2  10203  compsscnv  10355  fin1a2lem12  10395  mulerpqlem  10940  1lt2nq  10958  axi2m1  11144  2p2e4  12375  numsuc  12725  numsucc  12756  decmul10add  12785  5p5e10  12787  6p4e10  12788  7p3e10  12791  xnegmnf  13236  pnfaddmnf  13256  fz12pr  13609  fz0tp  13656  fz0to3un2pr  13657  fz0to4untppr  13658  fz0to5un2tp  13659  fzo13pr  13778  fzo0to2pr  13779  fz01pr  13780  fzo0to3tp  13781  fzo0to42pr  13782  fzo1to4tp  13783  fldiv4p1lem1div2  13868  sq4e2t8  14235  i4  14240  crreczi  14264  fac1  14313  fac3  14316  hashkf  14368  hashinf  14371  dmhashres  14377  hashun3  14420  dmtrclfv  15055  abs0  15336  absi  15337  trirecip  15917  geoihalfsum  15936  esum  16134  tan0  16207  coshval  16211  ef01bndlem  16240  3dvds  16389  3dvdsdec  16390  3dvds2dec  16391  sadc0  16512  3lcm2e6woprm  16673  6lcm4e12  16674  lcmf0  16692  prmo0  17096  gcdmodi  17134  karatsuba  17143  43prm  17182  139prm  17184  631prm  17187  1259lem1  17191  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  2503lem1  17197  2503lem2  17198  2503lem3  17199  4001lem1  17201  4001lem2  17202  4001lem3  17203  4001lem4  17204  setsfun  17231  setsfun0  17232  ndxarg  17256  chnccat  18682  ex-chn2  18694  pmtrsn  19589  psgnprfval1  19592  sylow2a  19689  ablfac1eu  20145  sralem  21275  pzriprng1ALT  21615  opsrtoslem2  22176  ply1plusgfvi  22370  pf1rcl  22478  restcld  23298  neitr  23306  txbasval  23732  txindis  23760  cnmpt1st  23794  cnmpt2nd  23795  ufildr  24057  restmetu  24696  cphipval2  25369  reust  25509  ehl0base  25544  ismbl  25654  mbfimaopnlem  25783  itg10  25816  itg2cnlem2  25890  itgz  25909  dvmptid  26085  cos2pi  26607  tan4thpi  26645  tan4thpiOLD  26646  sincos6thpi  26647  pige3ALT  26651  dfrelog  26696  logm1  26720  dvlog  26782  efopnlem2  26788  cxpexp  26799  root1id  26885  sqrt2cxp2logb9e3  26930  ang180lem2  26941  1cubrlem  26972  quart1  26987  atandm2  27008  efiasin  27019  asinsinlem  27022  asinsin  27023  asin1  27025  acos1  27026  atancj  27041  atanlogsublem  27046  efiatan2  27048  2efiatan  27049  tanatan  27050  dvatan  27066  log2cnv  27075  log2ublem2  27078  log2ublem3  27079  birthday  27085  basellem8  27218  cht1  27295  chp1  27297  ppi1i  27298  ppi2i  27299  cht2  27302  cht3  27303  bclbnd  27410  bposlem8  27421  2lgslem3c  27528  2lgslem3d  27529  noetasuplem2  27864  noetasuplem3  27865  noetasuplem4  27866  noetainflem4  27870  bday0  27970  old0  27998  new0  28023  left1s  28054  right1s  28055  ltslpss  28067  leslss  28068  mulsproplem13  28287  mulsproplem14  28288  precsexlem1  28366  precsexlem2  28367  oniso  28430  bdayn0sf1o  28529  ax5seglem7  29226  axlowdimlem8  29240  axlowdimlem11  29243  vtxvalsnop  29332  iedgvalsnop  29333  umgrislfupgrlem  29413  usgrexmpledg  29553  usgredgffibi  29615  vdegp1bi  29828  edginwlk  29925  uhgrwkspthlem2  30044  clwwlkvbij  30405  wlk2v2elem2  30448  frgrwopreglem3  30606  ex-dif  30715  ex-xp  30728  ex-rn  30732  ex-lcm  30750  ex-prmo  30751  ip0i  31118  ip1ilem  31119  ipdirilem  31122  ipasslem10  31132  hvnegdii  31355  hvaddcani  31358  hvsubaddi  31359  hisubcomi  31397  normlem0  31402  normlem3  31405  normlem9  31411  bcseqi  31413  norm0  31421  norm-ii-i  31430  norm3difi  31440  normpari  31447  normpar2i  31449  polid2i  31450  shs0i  31742  chj0i  31748  pjsslem  31972  ho0subi  32088  hoaddsubi  32114  hosd1i  32115  hopncani  32117  nmop0  32279  nmfn0  32280  lnopunilem1  32303  lnophmlem2  32310  opsqrlem2  32434  pjclem1  32488  atabsi  32694  dmdbr6ati  32716  inin  32803  iuninc  32846  gtiso  32987  f1od2  33005  fpwrelmapffs  33020  fzodif1  33078  nn0split01  33103  dfdec100  33115  dp20u  33138  dp3mul10  33158  dpmul1000  33159  dpexpp1  33168  dpadd2  33170  dpmul  33173  dpmul4  33174  1mhdrd  33176  cycpmrn  33404  tocyccntz  33405  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  lmat22det  34157  ordtcnvNEW  34255  ordtrest2NEW  34258  zlmtset  34298  qqhucn  34327  esumnul  34383  mbfmcst  34594  carsggect  34653  eulerpartgbij  34707  eulerpartlemn  34716  fib0  34734  fib1  34735  fib2  34737  fib3  34738  fib4  34739  fib5  34740  fib6  34741  0rrv  34786  coinflipprob  34815  ballotlem2  34824  ballotth  34873  signsvf0  34912  itgexpif  34938  hgt750lem  34983  hgt750lem2  34984  bnj1416  35372  r11  35430  r12  35431  derang0  35560  subfac0  35568  subfac1  35569  satfv1  35754  fmla  35772  fmla0  35773  fmla0xp  35774  fmla1  35778  mthmpps  35973  problem2  36057  quad3  36061  dfrdg2  36184  pprodcnveq  36272  dffv5  36313  dfsuccf2  36332  fullfunfv  36338  ellines  36543  rankeq1o  36562  onint1  36849  bj-xpimasn  37479  bj-pr11val  37529  bj-pr21val  37537  bj-pr22val  37543  bj-nuliotaALT  37582  bj-dfmpoa  37648  bj-opabco  37720  icorempo  37885  finxpreclem4  37928  finxp2o  37933  finxp3o  37934  matunitlindf  38157  poimirlem5  38164  poimirlem22  38181  poimirlem26  38185  poimirlem30  38189  ismblfin  38200  dvtan  38209  asindmre  38242  dvasin  38243  dvacos  38244  areacirclem5  38251  heiborlem6  38355  dmcnvep  38927  dmxrncnvep  38928  dmcnvepres  38929  dmxrnuncnvepres  38931  xrnres4  38967  dfadjliftmap2  38996  blockadjliftmap  38997  dfblockliftmap2  39000  dfsucmap3  39002  dfsuccl2  39009  dfcoels  39059  coss0  39108  refsymrels2  39188  dfeqvrels2  39211  refrelsredund4  39255  hdmap1cbv  42466  lcm4un  42673  lcm5un  42674  lcm6un  42675  lcm7un  42676  lcm8un  42677  3lexlogpow5ineq1  42711  5bc2eq10  42799  imaopab  42892  decpmul  42939  cxpi11d  42994  tan3rdpi  43003  sin2t3rdpi  43004  cos2t3rdpi  43005  readvrec2  43012  remul02  43056  fltnltalem  43286  sum9cubes  43296  diophrw  43382  dnwech  43667  lmhmlnmsplit  43706  fgraphopab  43822  arearect  43834  areaquad  43835  oaomoencom  43936  dmnonrel  44208  imanonrel  44211  cononrel1  44212  cononrel2  44213  rclexi  44233  rtrclex  44235  dfrtrcl5  44247  sqrtcval  44259  resqrtvalex  44263  imsqrtvalex  44264  cnvtrrel  44288  dfrcl2  44292  dfrcl4  44294  iunrelexp0  44320  comptiunov2i  44324  relexpaddss  44336  brtrclfv2  44345  trclfvdecomr  44346  corcltrcl  44357  cotrclrcl  44360  fsovcnvlem  44631  neicvgnvo  44733  mnuprdlem1  44874  hashnzfz  44922  lhe4.4ex1a  44931  tgqioo2  46155  sumnnodd  46238  limsup0  46300  limsup10ex  46379  liminf10ex  46380  cosnegpi  46473  itgsin0pilem1  46556  stoweidlem13  46619  wallispilem4  46674  wallispi2lem1  46677  wallispi2lem2  46678  stirlinglem3  46682  dirkertrigeqlem1  46704  fourierdlem56  46768  fourierdlem57  46769  fourierdlem58  46770  fourierdlem62  46774  fourierdlem103  46815  fourierdlem104  46816  fourierdlem112  46824  sqwvfoura  46834  fouriersw  46837  etransclem23  46863  etransclem36  46876  etransclem38  46878  carageniuncllem1  47127  0ome  47135  ovn02  47174  smflimlem4  47380  smflim  47383  smflim2  47412  smflimsup  47434  smfliminf  47437  cos5t  47505  goldratmolem2  47512  fmtno0  48181  fmtno1  48182  fmtno2  48191  fmtno3  48192  fmtno4  48193  fmtno5lem4  48197  139prmALT  48237  31prm  48238  5tcu2e40  48256  3exp4mod41  48257  41prothprmlem2  48259  41prothprm  48260  ppivalnn4  48268  nnsum3primesgbe  48446  nnsum4primesodd  48450  nnsum4primesoddALTV  48451  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  bgoldbtbndlem1  48459  tgoldbachlt  48470  isuspgrim0lem  48547  isubgr3stgrlem4  48623  isubgr3stgrlem6  48625  isubgr3stgrlem7  48626  usgrexmpl1vtx  48677  usgrexmpl1edg  48678  usgrexmpl2vtx  48682  usgrexmpl2edg  48683  gpg5gricstgr3  48744  gpgprismgr4cycllem7  48755  cznrnglem  48913  2t6m3t4e0  49013  zlmodzxzldeplem3  49167  ackval0  49345  ackval1  49346  ackval2  49347  ackval3  49348  ackval40  49358  ackval42  49361  ackval50  49363  disjdifb  49473  dftpos6  49538  tposresg  49541  tposrescnv  49542  tposres3  49544  tposid  49548  iscnrm3rlem1  49603  dfswapf2  49924  setc1onsubc  50265  sec0  50423