Theorem 3eqtri 2761

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726

This theorem is referenced by:  csbid  3885  csbconstg  3891  csbie  3907  un23  4147  in32  4203  dfnul4  4308  unvdif  4448  undif2  4450  undifabs  4451  difun2  4454  difdifdir  4465  dfif4  4514  dfif5  4515  tpidm23  4730  dfopif  4843  dfiunv2  5008  symdif0  5058  symdifid  5060  unidif0  5327  uniop  5487  xpun  5725  dfrn2  5865  dfdmf  5873  dfrnf  5927  res0  5967  resres  5976  xpssres  6002  dfima2  6046  imai  6058  ima0  6061  imaundir  6136  xpima  6168  cnvrescnv  6181  dmresv  6186  rescnvcnv  6190  dmtpop  6204  rnsnopg  6207  resdmres  6218  resdifdi  6222  dmmpt  6226  dmco  6240  co01  6247  suc0  6425  iunsuc  6435  fresaun  6745  dffv4  6869  fvssunirnOLD  6906  f1ossf1o  7114  fpr  7140  mpo0  7486  dmoprab  7504  rnoprab  7506  elrnmpores  7539  ov6g  7565  1st0  7988  2nd0  7989  dfmpo  8095  curry1  8097  curry2  8100  fpar  8109  dftpos2  8236  tposoprab  8255  tposmpo  8256  fvmpocurryd  8264  frrlem14  8292  dfwrecsOLD  8306  wfrlem14OLD  8330  wfrlem16OLD  8332  dfrecs3  8380  dfrecs3OLD  8381  tfrlem8  8392  seqomlem3  8460  df2o3  8482  nlim2  8496  omxpenlem  9081  dfsdom2  9104  pwfir  9321  marypha2lem2  9442  sup00  9470  epinid0  9606  scottexs  9893  scott0s  9894  infxpenc2  10028  kmlem3  10159  ackbij1lem2  10226  compsscnv  10377  fin1a2lem12  10417  mulerpqlem  10961  1lt2nq  10979  axi2m1  11165  2p2e4  12367  numsuc  12714  numsucc  12740  decmul10add  12769  5p5e10  12771  6p4e10  12772  7p3e10  12775  xnegmnf  13218  pnfaddmnf  13238  fz12pr  13587  fz0tp  13634  fz0to3un2pr  13635  fz0to4untppr  13636  fz0to5un2tp  13637  fzo13pr  13754  fzo0to2pr  13755  fz01pr  13756  fzo0to3tp  13757  fzo0to42pr  13758  fzo1to4tp  13759  fldiv4p1lem1div2  13841  sq4e2t8  14205  i4  14210  crreczi  14234  fac1  14283  fac3  14286  hashkf  14338  hashinf  14341  dmhashres  14347  hashun3  14390  cshwsexaOLD  14830  dmtrclfv  15024  abs0  15291  absi  15292  trirecip  15866  geoihalfsum  15885  esum  16083  tan0  16154  coshval  16158  ef01bndlem  16187  3dvds  16335  3dvdsdec  16336  3dvds2dec  16337  sadc0  16458  3lcm2e6woprm  16619  6lcm4e12  16620  lcmf0  16638  prmo0  17041  gcdmodi  17079  karatsuba  17088  43prm  17126  139prm  17128  631prm  17131  1259lem1  17135  1259lem2  17136  1259lem3  17137  1259lem4  17138  1259lem5  17139  2503lem1  17141  2503lem2  17142  2503lem3  17143  4001lem1  17145  4001lem2  17146  4001lem3  17147  4001lem4  17148  setsfun  17175  setsfun0  17176  ndxarg  17200  pmtrsn  19485  psgnprfval1  19488  sylow2a  19585  ablfac1eu  20041  sralem  21119  pzriprng1ALT  21442  opsrtoslem2  21999  ply1plusgfvi  22162  pf1rcl  22272  restcld  23095  neitr  23103  txbasval  23529  txindis  23557  cnmpt1st  23591  cnmpt2nd  23592  ufildr  23854  restmetu  24494  cphipval2  25178  reust  25318  ehl0base  25353  ismbl  25464  mbfimaopnlem  25593  itg10  25626  itg2cnlem2  25700  itgz  25719  dvmptid  25898  cos2pi  26421  tan4thpi  26459  tan4thpiOLD  26460  sincos6thpi  26461  pige3ALT  26465  dfrelog  26510  logm1  26534  dvlog  26596  efopnlem2  26602  cxpexp  26613  root1id  26700  sqrt2cxp2logb9e3  26745  ang180lem2  26756  1cubrlem  26787  quart1  26802  atandm2  26823  efiasin  26834  asinsinlem  26837  asinsin  26838  asin1  26840  acos1  26841  atancj  26856  atanlogsublem  26861  efiatan2  26863  2efiatan  26864  tanatan  26865  dvatan  26881  log2cnv  26890  log2ublem2  26893  log2ublem3  26894  birthday  26900  basellem8  27034  cht1  27111  chp1  27113  ppi1i  27114  ppi2i  27115  cht2  27118  cht3  27119  bclbnd  27227  bposlem8  27238  2lgslem3c  27345  2lgslem3d  27346  noetasuplem2  27682  noetasuplem3  27683  noetasuplem4  27684  noetainflem4  27688  bday0s  27776  old0  27801  new0  27816  left1s  27836  right1s  27837  sltlpss  27848  slelss  27849  mulsproplem13  28057  mulsproplem14  28058  precsexlem1  28134  precsexlem2  28135  ax5seglem7  28846  axlowdimlem8  28860  axlowdimlem11  28863  vtxvalsnop  28952  iedgvalsnop  28953  umgrislfupgrlem  29033  usgrexmpledg  29173  usgredgffibi  29235  vdegp1bi  29449  edginwlk  29547  uhgrwkspthlem2  29668  clwwlkvbij  30026  wlk2v2elem2  30069  frgrwopreglem3  30227  ex-dif  30336  ex-xp  30349  ex-rn  30353  ex-lcm  30371  ex-prmo  30372  ip0i  30738  ip1ilem  30739  ipdirilem  30742  ipasslem10  30752  hvnegdii  30975  hvaddcani  30978  hvsubaddi  30979  hisubcomi  31017  normlem0  31022  normlem3  31025  normlem9  31031  bcseqi  31033  norm0  31041  norm-ii-i  31050  norm3difi  31060  normpari  31067  normpar2i  31069  polid2i  31070  shs0i  31362  chj0i  31368  pjsslem  31592  ho0subi  31708  hoaddsubi  31734  hosd1i  31735  hopncani  31737  nmop0  31899  nmfn0  31900  lnopunilem1  31923  lnophmlem2  31930  opsqrlem2  32054  pjclem1  32108  atabsi  32314  dmdbr6ati  32336  inin  32429  iuninc  32474  gtiso  32611  f1od2  32633  fpwrelmapffs  32646  fzodif1  32703  nn0split01  32729  dfdec100  32742  dp20u  32770  dp3mul10  32790  dpmul1000  32791  dpexpp1  32800  dpadd2  32802  dpmul  32805  dpmul4  32806  1mhdrd  32808  cycpmrn  33072  tocyccntz  33073  lmat22det  33761  ordtcnvNEW  33859  ordtrest2NEW  33862  zlmtset  33902  qqhucn  33931  esumnul  33987  mbfmcst  34199  carsggect  34258  eulerpartgbij  34312  eulerpartlemn  34321  fib0  34339  fib1  34340  fib2  34342  fib3  34343  fib4  34344  fib5  34345  fib6  34346  0rrv  34391  coinflipprob  34420  ballotlem2  34429  ballotth  34478  signsvf0  34533  itgexpif  34559  hgt750lem  34604  hgt750lem2  34605  bnj1416  34991  derang0  35112  subfac0  35120  subfac1  35121  satfv1  35306  fmla  35324  fmla0  35325  fmla0xp  35326  fmla1  35330  mthmpps  35525  problem2  35609  quad3  35613  dfrdg2  35734  pprodcnveq  35822  dffv5  35863  fullfunfv  35886  ellines  36091  rankeq1o  36110  onint1  36388  bj-xpimasn  36894  bj-pr11val  36944  bj-pr21val  36952  bj-pr22val  36958  bj-nuliotaALT  36997  bj-dfmpoa  37057  bj-opabco  37127  icorempo  37290  finxpreclem4  37333  finxp2o  37338  finxp3o  37339  matunitlindf  37563  poimirlem5  37570  poimirlem22  37587  poimirlem26  37591  poimirlem30  37595  ismblfin  37606  dvtan  37615  asindmre  37648  dvasin  37649  dvacos  37650  areacirclem5  37657  heiborlem6  37761  xrnres4  38344  dfcoels  38369  coss0  38418  refsymrels2  38504  dfeqvrels2  38527  refrelsredund4  38571  hdmap1cbv  41742  lcm4un  41951  lcm5un  41952  lcm6un  41953  lcm7un  41954  lcm8un  41955  3lexlogpow5ineq1  41989  5bc2eq10  42077  2xp3dxp2ge1d  42176  imaopab  42204  decpmul  42261  cxpi11d  42317  tan3rdpi  42324  readvrec2  42329  remul02  42373  fltnltalem  42610  sum9cubes  42620  diophrw  42707  dnwech  42997  lmhmlnmsplit  43036  fgraphopab  43152  arearect  43164  areaquad  43165  oaomoencom  43266  dmnonrel  43539  imanonrel  43542  cononrel1  43543  cononrel2  43544  rclexi  43564  rtrclex  43566  dfrtrcl5  43578  sqrtcval  43590  resqrtvalex  43594  imsqrtvalex  43595  cnvtrrel  43619  dfrcl2  43623  dfrcl4  43625  iunrelexp0  43651  comptiunov2i  43655  relexpaddss  43667  brtrclfv2  43676  trclfvdecomr  43677  corcltrcl  43688  cotrclrcl  43691  fsovcnvlem  43962  neicvgnvo  44064  scottabf  44190  mnuprdlem1  44222  hashnzfz  44270  lhe4.4ex1a  44279  tgqioo2  45504  sumnnodd  45589  limsup0  45653  limsup10ex  45732  liminf10ex  45733  cosnegpi  45826  itgsin0pilem1  45909  stoweidlem13  45972  wallispilem4  46027  wallispi2lem1  46030  wallispi2lem2  46031  stirlinglem3  46035  dirkertrigeqlem1  46057  fourierdlem56  46121  fourierdlem57  46122  fourierdlem58  46123  fourierdlem62  46127  fourierdlem103  46168  fourierdlem104  46169  fourierdlem112  46177  sqwvfoura  46187  fouriersw  46190  etransclem23  46216  etransclem36  46229  etransclem38  46231  carageniuncllem1  46480  0ome  46488  ovn02  46527  smflimlem4  46733  smflim  46736  smflim2  46765  smflimsup  46787  smfliminf  46790  fmtno0  47472  fmtno1  47473  fmtno2  47482  fmtno3  47483  fmtno4  47484  fmtno5lem4  47488  139prmALT  47528  31prm  47529  5tcu2e40  47547  3exp4mod41  47548  41prothprmlem2  47550  41prothprm  47551  nnsum3primesgbe  47724  nnsum4primesodd  47728  nnsum4primesoddALTV  47729  nnsum4primeseven  47732  nnsum4primesevenALTV  47733  bgoldbtbndlem1  47737  tgoldbachlt  47748  isuspgrim0lem  47816  isubgr3stgrlem4  47881  isubgr3stgrlem6  47883  isubgr3stgrlem7  47884  usgrexmpl1vtx  47927  usgrexmpl1edg  47928  usgrexmpl2vtx  47932  usgrexmpl2edg  47933  gpg5gricstgr3  47991  cznrnglem  48120  2t6m3t4e0  48209  zlmodzxzldeplem3  48364  ackval0  48546  ackval1  48547  ackval2  48548  ackval3  48549  ackval40  48559  ackval42  48562  ackval50  48564  disjdifb  48674  dftpos6  48730  tposresg  48733  tposrescnv  48734  tposres3  48736  tposid  48740  iscnrm3rlem1  48793  dfswapf2  48984  sec0  49344