Theorem 3eqtri 2848

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

Syntax hints:   = wceq 1537

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  csbid  3896  un23  4144  in32  4198  dfnul2  4293  unvdif  4423  undif2  4425  undifabs  4426  difun2  4429  difdifdir  4437  dfif4  4482  dfif5  4483  tpidm23  4693  dfopif  4800  dfiunv2  4960  symdif0  5007  symdifid  5009  unidif0  5260  uniop  5405  xpun  5625  dfrn2  5759  dfdmf  5765  dfrnf  5820  res0  5857  resres  5866  xpssres  5889  dfima2  5931  imai  5942  ima0  5945  imaundir  6009  xpima  6039  cnvrescnv  6052  dmresv  6057  rescnvcnv  6061  dmtpop  6075  rnsnopg  6078  resdmres  6089  dmmpt  6094  dmco  6107  co01  6114  suc0  6265  unisuc  6267  iunsuc  6273  fresaun  6549  dffv4  6667  fvssunirn  6699  f1ossf1o  6890  fpr  6916  mpo0  7239  dmoprab  7255  rnoprab  7257  elrnmpores  7288  ov6g  7312  1st0  7695  2nd0  7696  dfmpo  7797  curry1  7799  curry2  7802  fpar  7811  algrflem  7819  dftpos2  7909  tposoprab  7928  tposmpo  7929  fvmpocurryd  7937  wfrlem14  7968  wfrlem16  7970  dfrecs3  8009  tfrlem8  8020  seqomlem3  8088  df2o3  8117  omxpenlem  8618  dfsdom2  8640  marypha2lem2  8900  sup00  8928  epinid0  9064  scottexs  9316  scott0s  9317  infxpenc2  9448  kmlem3  9578  ackbij1lem2  9643  compsscnv  9793  fin1a2lem12  9833  mulerpqlem  10377  1lt2nq  10395  axi2m1  10581  2p2e4  11773  numsuc  12113  numsucc  12139  decmul10add  12168  5p5e10  12170  6p4e10  12171  7p3e10  12174  xnegmnf  12604  pnfaddmnf  12624  fz12pr  12965  fz0tp  13009  fz0to3un2pr  13010  fzo13pr  13122  fzo0to2pr  13123  fzo0to3tp  13124  fzo0to42pr  13125  fzo1to4tp  13126  fldiv4p1lem1div2  13206  sq4e2t8  13563  i4  13568  crreczi  13590  fac1  13638  fac3  13641  hashkf  13693  hashinf  13696  dmhashres  13702  hashun3  13746  cshwsexa  14186  dmtrclfv  14378  abs0  14645  absi  14646  trirecip  15218  geoihalfsum  15238  esum  15434  tan0  15504  coshval  15508  ef01bndlem  15537  3dvds  15680  3dvdsdec  15681  3dvds2dec  15682  sadc0  15803  3lcm2e6woprm  15959  6lcm4e12  15960  lcmf0  15978  prmo0  16372  gcdmodi  16410  karatsuba  16420  43prm  16455  139prm  16457  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem1  16470  2503lem2  16471  2503lem3  16472  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  ndxarg  16508  setsfun  16518  setsfun0  16519  pmtrsn  18647  psgnprfval1  18650  sylow2a  18744  ablfac1eu  19195  sralem  19949  opsrtoslem2  20265  ply1plusgfvi  20410  pf1rcl  20512  restcld  21780  neitr  21788  txbasval  22214  txindis  22242  cnmpt1st  22276  cnmpt2nd  22277  ufildr  22539  restmetu  23180  cphipval2  23844  reust  23984  ehl0base  24019  ismbl  24127  mbfimaopnlem  24256  itg10  24289  itg2cnlem2  24363  itgz  24381  dvmptid  24554  cos2pi  25062  tan4thpi  25100  sincos6thpi  25101  pige3ALT  25105  dfrelog  25149  logm1  25172  dvlog  25234  efopnlem2  25240  cxpexp  25251  root1id  25335  sqrt2cxp2logb9e3  25377  ang180lem2  25388  1cubrlem  25419  quart1  25434  atandm2  25455  efiasin  25466  asinsinlem  25469  asinsin  25470  asin1  25472  acos1  25473  atancj  25488  atanlogsublem  25493  efiatan2  25495  2efiatan  25496  tanatan  25497  dvatan  25513  log2cnv  25522  log2ublem2  25525  log2ublem3  25526  birthday  25532  basellem8  25665  cht1  25742  chp1  25744  ppi1i  25745  ppi2i  25746  cht2  25749  cht3  25750  bclbnd  25856  bposlem8  25867  2lgslem3c  25974  2lgslem3d  25975  ax5seglem7  26721  axlowdimlem8  26735  axlowdimlem11  26738  vtxvalsnop  26826  iedgvalsnop  26827  umgrislfupgrlem  26907  usgrexmpledg  27044  usgredgffibi  27106  vdegp1bi  27319  edginwlk  27416  uhgrwkspthlem2  27535  clwwlkvbij  27892  wlk2v2elem2  27935  frgrwopreglem3  28093  ex-dif  28202  ex-xp  28215  ex-rn  28219  ex-lcm  28237  ex-prmo  28238  ip0i  28602  ip1ilem  28603  ipdirilem  28606  ipasslem10  28616  hvnegdii  28839  hvaddcani  28842  hvsubaddi  28843  hisubcomi  28881  normlem0  28886  normlem3  28889  normlem9  28895  bcseqi  28897  norm0  28905  norm-ii-i  28914  norm3difi  28924  normpari  28931  normpar2i  28933  polid2i  28934  shs0i  29226  chj0i  29232  pjsslem  29456  ho0subi  29572  hoaddsubi  29598  hosd1i  29599  hopncani  29601  nmop0  29763  nmfn0  29764  lnopunilem1  29787  lnophmlem2  29794  opsqrlem2  29918  pjclem1  29972  atabsi  30178  dmdbr6ati  30200  inin  30277  iuninc  30312  gtiso  30436  f1od2  30457  fpwrelmapffs  30470  fzodif1  30516  dfdec100  30546  dp20u  30554  dp3mul10  30574  dpmul1000  30575  dpexpp1  30584  dpadd2  30586  dpmul  30589  dpmul4  30590  1mhdrd  30592  cycpmrn  30785  tocyccntz  30786  lmat22det  31087  ordtcnvNEW  31163  ordtrest2NEW  31166  zlmtset  31206  qqhucn  31233  esumnul  31307  mbfmcst  31517  carsggect  31576  eulerpartgbij  31630  eulerpartlemn  31639  fib0  31657  fib1  31658  fib2  31660  fib3  31661  fib4  31662  fib5  31663  fib6  31664  0rrv  31709  coinflipprob  31737  ballotlem2  31746  ballotth  31795  signsvf0  31850  itgexpif  31877  hgt750lem  31922  hgt750lem2  31923  bnj1416  32311  derang0  32416  subfac0  32424  subfac1  32425  satfv1  32610  fmla  32628  fmla0  32629  fmla0xp  32630  fmla1  32634  mthmpps  32829  problem2  32909  quad3  32913  dfrdg2  33040  trpred0  33075  frrlem14  33136  noetalem2  33218  noetalem3  33219  pprodcnveq  33344  dffv5  33385  fullfunfv  33408  ellines  33613  rankeq1o  33632  onint1  33797  bj-xpimasn  34270  bj-pr11val  34320  bj-pr21val  34328  bj-pr22val  34334  bj-nuliotaALT  34354  bj-dfmpoa  34413  icorempo  34635  finxpreclem4  34678  finxp2o  34683  finxp3o  34684  matunitlindf  34905  poimirlem5  34912  poimirlem22  34929  poimirlem26  34933  poimirlem30  34937  ismblfin  34948  dvtan  34957  asindmre  34992  dvasin  34993  dvacos  34994  areacirclem5  35001  heiborlem6  35109  xrnres4  35668  dfcoels  35690  coss0  35734  refsymrels2  35816  dfeqvrels2  35838  refrelsredund4  35882  hdmap1cbv  38953  lcm4un  39137  lcm5un  39138  lcm6un  39139  lcm7un  39140  lcm8un  39141  2xp3dxp2ge1d  39146  imaopab  39168  sqn5ii  39221  decpmul  39223  remul02  39284  sn-0lt1  39295  fltnltalem  39323  diophrw  39405  dnwech  39697  lmhmlnmsplit  39736  fgraphopab  39859  arearect  39871  areaquad  39872  dmnonrel  39999  imanonrel  40002  cononrel1  40003  cononrel2  40004  rclexi  40024  rtrclex  40026  dfrtrcl5  40038  cnvtrrel  40064  dfrcl2  40068  dfrcl4  40070  iunrelexp0  40096  comptiunov2i  40100  relexpaddss  40112  brtrclfv2  40121  trclfvdecomr  40122  corcltrcl  40133  cotrclrcl  40136  fsovcnvlem  40408  neicvgnvo  40514  scottabf  40625  mnuprdlem1  40657  hashnzfz  40701  lhe4.4ex1a  40710  disjinfi  41503  tgqioo2  41872  sumnnodd  41960  limsup0  42024  limsup10ex  42103  liminf10ex  42104  cosnegpi  42197  itgsin0pilem1  42284  stoweidlem13  42347  wallispilem4  42402  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem3  42410  dirkertrigeqlem1  42432  fourierdlem56  42496  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  sqwvfoura  42562  fouriersw  42565  etransclem23  42591  etransclem36  42604  etransclem38  42606  carageniuncllem1  42852  0ome  42860  ovn02  42899  smflimlem4  43099  smflim  43102  smflim2  43129  smflimsup  43151  smfliminf  43154  fmtno0  43751  fmtno1  43752  fmtno2  43761  fmtno3  43762  fmtno4  43763  fmtno5lem4  43767  139prmALT  43808  31prm  43809  5tcu2e40  43829  3exp4mod41  43830  41prothprmlem2  43832  41prothprm  43833  nnsum3primesgbe  44006  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  tgoldbachlt  44030  cznrnglem  44273  2t6m3t4e0  44445  zlmodzxzldeplem3  44606  sec0  44908