Theorem 3eqtri 2760

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

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

This theorem is referenced by:  csbid  3859  csbconstg  3865  csbie  3881  un23  4123  in32  4179  dfnul4  4284  unvdif  4424  undif2  4426  undifabs  4427  difun2  4430  difdifdir  4441  dfif4  4492  dfif5  4493  tpidm23  4711  dfopif  4823  dfiunv2  4986  symdif0  5037  symdifid  5039  unidif0  5302  uniop  5460  xpun  5695  dfrn2  5834  dfdmf  5842  dfrnf  5896  res0  5939  resres  5948  xpssres  5974  dfima2  6018  imai  6030  ima0  6033  imaundir  6105  xpima  6137  cnvrescnv  6150  dmresv  6155  rescnvcnv  6159  dmtpop  6173  rnsnopg  6176  resdmres  6187  resdifdi  6191  dmmpt  6195  dmco  6210  co01  6217  suc0  6391  iunsuc  6401  fresaun  6702  dffv4  6828  f1ossf1o  7070  fpr  7096  mpo0  7440  dmoprab  7458  rnoprab  7460  elrnmpores  7493  ov6g  7519  1st0  7936  2nd0  7937  dfmpo  8041  curry1  8043  curry2  8046  fpar  8055  dftpos2  8182  tposoprab  8201  tposmpo  8202  fvmpocurryd  8210  frrlem14  8238  dfrecs3  8301  tfrlem8  8312  seqomlem3  8380  df2o3  8402  nlim2  8414  omxpenlem  9002  dfsdom2  9024  pwfir  9212  marypha2lem2  9331  sup00  9360  epinid0  9500  scottexs  9791  scott0s  9792  infxpenc2  9924  kmlem3  10055  ackbij1lem2  10122  compsscnv  10273  fin1a2lem12  10313  mulerpqlem  10857  1lt2nq  10875  axi2m1  11061  2p2e4  12266  numsuc  12612  numsucc  12638  decmul10add  12667  5p5e10  12669  6p4e10  12670  7p3e10  12673  xnegmnf  13116  pnfaddmnf  13136  fz12pr  13488  fz0tp  13535  fz0to3un2pr  13536  fz0to4untppr  13537  fz0to5un2tp  13538  fzo13pr  13656  fzo0to2pr  13657  fz01pr  13658  fzo0to3tp  13659  fzo0to42pr  13660  fzo1to4tp  13661  fldiv4p1lem1div2  13746  sq4e2t8  14113  i4  14118  crreczi  14142  fac1  14191  fac3  14194  hashkf  14246  hashinf  14249  dmhashres  14255  hashun3  14298  dmtrclfv  14932  abs0  15199  absi  15200  trirecip  15777  geoihalfsum  15796  esum  15994  tan0  16067  coshval  16071  ef01bndlem  16100  3dvds  16249  3dvdsdec  16250  3dvds2dec  16251  sadc0  16372  3lcm2e6woprm  16533  6lcm4e12  16534  lcmf0  16552  prmo0  16955  gcdmodi  16993  karatsuba  17002  43prm  17040  139prm  17042  631prm  17045  1259lem1  17049  1259lem2  17050  1259lem3  17051  1259lem4  17052  1259lem5  17053  2503lem1  17055  2503lem2  17056  2503lem3  17057  4001lem1  17059  4001lem2  17060  4001lem3  17061  4001lem4  17062  setsfun  17089  setsfun0  17090  ndxarg  17114  chnccat  18540  ex-chn2  18552  pmtrsn  19439  psgnprfval1  19442  sylow2a  19539  ablfac1eu  19995  sralem  21119  pzriprng1ALT  21442  opsrtoslem2  22002  ply1plusgfvi  22173  pf1rcl  22284  restcld  23107  neitr  23115  txbasval  23541  txindis  23569  cnmpt1st  23603  cnmpt2nd  23604  ufildr  23866  restmetu  24505  cphipval2  25188  reust  25328  ehl0base  25363  ismbl  25474  mbfimaopnlem  25603  itg10  25636  itg2cnlem2  25710  itgz  25729  dvmptid  25908  cos2pi  26432  tan4thpi  26470  tan4thpiOLD  26471  sincos6thpi  26472  pige3ALT  26476  dfrelog  26521  logm1  26545  dvlog  26607  efopnlem2  26613  cxpexp  26624  root1id  26711  sqrt2cxp2logb9e3  26756  ang180lem2  26767  1cubrlem  26798  quart1  26813  atandm2  26834  efiasin  26845  asinsinlem  26848  asinsin  26849  asin1  26851  acos1  26852  atancj  26867  atanlogsublem  26872  efiatan2  26874  2efiatan  26875  tanatan  26876  dvatan  26892  log2cnv  26901  log2ublem2  26904  log2ublem3  26905  birthday  26911  basellem8  27045  cht1  27122  chp1  27124  ppi1i  27125  ppi2i  27126  cht2  27129  cht3  27130  bclbnd  27238  bposlem8  27249  2lgslem3c  27356  2lgslem3d  27357  noetasuplem2  27693  noetasuplem3  27694  noetasuplem4  27695  noetainflem4  27699  bday0s  27792  old0  27820  new0  27839  left1s  27860  right1s  27861  sltlpss  27873  slelss  27874  mulsproplem13  28087  mulsproplem14  28088  precsexlem1  28165  precsexlem2  28166  onsiso  28225  bdayn0sf1o  28315  ax5seglem7  28934  axlowdimlem8  28948  axlowdimlem11  28951  vtxvalsnop  29040  iedgvalsnop  29041  umgrislfupgrlem  29121  usgrexmpledg  29261  usgredgffibi  29323  vdegp1bi  29537  edginwlk  29634  uhgrwkspthlem2  29753  clwwlkvbij  30114  wlk2v2elem2  30157  frgrwopreglem3  30315  ex-dif  30424  ex-xp  30437  ex-rn  30441  ex-lcm  30459  ex-prmo  30460  ip0i  30826  ip1ilem  30827  ipdirilem  30830  ipasslem10  30840  hvnegdii  31063  hvaddcani  31066  hvsubaddi  31067  hisubcomi  31105  normlem0  31110  normlem3  31113  normlem9  31119  bcseqi  31121  norm0  31129  norm-ii-i  31138  norm3difi  31148  normpari  31155  normpar2i  31157  polid2i  31158  shs0i  31450  chj0i  31456  pjsslem  31680  ho0subi  31796  hoaddsubi  31822  hosd1i  31823  hopncani  31825  nmop0  31987  nmfn0  31988  lnopunilem1  32011  lnophmlem2  32018  opsqrlem2  32142  pjclem1  32196  atabsi  32402  dmdbr6ati  32424  inin  32517  iuninc  32561  gtiso  32706  f1od2  32726  fpwrelmapffs  32741  fzodif1  32800  nn0split01  32826  dfdec100  32839  dp20u  32887  dp3mul10  32907  dpmul1000  32908  dpexpp1  32917  dpadd2  32919  dpmul  32922  dpmul4  32923  1mhdrd  32925  cycpmrn  33153  tocyccntz  33154  cos9thpiminplylem4  33870  cos9thpiminplylem5  33871  lmat22det  33907  ordtcnvNEW  34005  ordtrest2NEW  34008  zlmtset  34048  qqhucn  34077  esumnul  34133  mbfmcst  34344  carsggect  34403  eulerpartgbij  34457  eulerpartlemn  34466  fib0  34484  fib1  34485  fib2  34487  fib3  34488  fib4  34489  fib5  34490  fib6  34491  0rrv  34536  coinflipprob  34565  ballotlem2  34574  ballotth  34623  signsvf0  34665  itgexpif  34691  hgt750lem  34736  hgt750lem2  34737  bnj1416  35123  r11  35177  r12  35178  derang0  35285  subfac0  35293  subfac1  35294  satfv1  35479  fmla  35497  fmla0  35498  fmla0xp  35499  fmla1  35503  mthmpps  35698  problem2  35782  quad3  35786  dfrdg2  35909  pprodcnveq  35997  dffv5  36038  dfsuccf2  36057  fullfunfv  36063  ellines  36268  rankeq1o  36287  onint1  36565  bj-xpimasn  37072  bj-pr11val  37122  bj-pr21val  37130  bj-pr22val  37136  bj-nuliotaALT  37175  bj-dfmpoa  37235  bj-opabco  37305  icorempo  37468  finxpreclem4  37511  finxp2o  37516  finxp3o  37517  matunitlindf  37731  poimirlem5  37738  poimirlem22  37755  poimirlem26  37759  poimirlem30  37763  ismblfin  37774  dvtan  37783  asindmre  37816  dvasin  37817  dvacos  37818  areacirclem5  37825  heiborlem6  37929  dmcnvep  38485  dmxrncnvep  38486  dmcnvepres  38487  dmxrnuncnvepres  38489  xrnres4  38525  dfadjliftmap2  38544  blockadjliftmap  38545  dfblockliftmap2  38547  dfsucmap3  38549  dfsuccl2  38556  dfcoels  38605  coss0  38654  refsymrels2  38734  dfeqvrels2  38757  refrelsredund4  38801  hdmap1cbv  41974  lcm4un  42182  lcm5un  42183  lcm6un  42184  lcm7un  42185  lcm8un  42186  3lexlogpow5ineq1  42220  5bc2eq10  42308  imaopab  42402  decpmul  42458  cxpi11d  42513  tan3rdpi  42522  sin2t3rdpi  42523  cos2t3rdpi  42524  readvrec2  42531  remul02  42575  fltnltalem  42820  sum9cubes  42830  diophrw  42916  dnwech  43205  lmhmlnmsplit  43244  fgraphopab  43360  arearect  43372  areaquad  43373  oaomoencom  43474  dmnonrel  43747  imanonrel  43750  cononrel1  43751  cononrel2  43752  rclexi  43772  rtrclex  43774  dfrtrcl5  43786  sqrtcval  43798  resqrtvalex  43802  imsqrtvalex  43803  cnvtrrel  43827  dfrcl2  43831  dfrcl4  43833  iunrelexp0  43859  comptiunov2i  43863  relexpaddss  43875  brtrclfv2  43884  trclfvdecomr  43885  corcltrcl  43896  cotrclrcl  43899  fsovcnvlem  44170  neicvgnvo  44272  scottabf  44397  mnuprdlem1  44429  hashnzfz  44477  lhe4.4ex1a  44486  tgqioo2  45709  sumnnodd  45792  limsup0  45854  limsup10ex  45933  liminf10ex  45934  cosnegpi  46027  itgsin0pilem1  46110  stoweidlem13  46173  wallispilem4  46228  wallispi2lem1  46231  wallispi2lem2  46232  stirlinglem3  46236  dirkertrigeqlem1  46258  fourierdlem56  46322  fourierdlem57  46323  fourierdlem58  46324  fourierdlem62  46328  fourierdlem103  46369  fourierdlem104  46370  fourierdlem112  46378  sqwvfoura  46388  fouriersw  46391  etransclem23  46417  etransclem36  46430  etransclem38  46432  carageniuncllem1  46681  0ome  46689  ovn02  46728  smflimlem4  46934  smflim  46937  smflim2  46966  smflimsup  46988  smfliminf  46991  fmtno0  47702  fmtno1  47703  fmtno2  47712  fmtno3  47713  fmtno4  47714  fmtno5lem4  47718  139prmALT  47758  31prm  47759  5tcu2e40  47777  3exp4mod41  47778  41prothprmlem2  47780  41prothprm  47781  nnsum3primesgbe  47954  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  nnsum4primeseven  47962  nnsum4primesevenALTV  47963  bgoldbtbndlem1  47967  tgoldbachlt  47978  isuspgrim0lem  48055  isubgr3stgrlem4  48131  isubgr3stgrlem6  48133  isubgr3stgrlem7  48134  usgrexmpl1vtx  48185  usgrexmpl1edg  48186  usgrexmpl2vtx  48190  usgrexmpl2edg  48191  gpg5gricstgr3  48252  gpgprismgr4cycllem7  48263  cznrnglem  48421  2t6m3t4e0  48510  zlmodzxzldeplem3  48664  ackval0  48842  ackval1  48843  ackval2  48844  ackval3  48845  ackval40  48855  ackval42  48858  ackval50  48860  disjdifb  48971  dftpos6  49036  tposresg  49039  tposrescnv  49040  tposres3  49042  tposid  49046  iscnrm3rlem1  49101  dfswapf2  49422  setc1onsubc  49763  sec0  49921