Theorem 3eqtri 2832

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

Syntax hints:   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  csbid  3736  un23  3971  in32  4022  unvdif  4238  undif2  4240  undifabs  4241  difun2  4244  difdifdir  4252  dfif4  4294  dfif5  4295  tpidm23  4483  dfopif  4592  unisnOLD  4647  dfiunv2  4748  symdif0  4789  symdifid  4791  unidif0  5030  uniop  5170  xpun  5376  dfrn2  5512  dfdmf  5518  dfrnf  5565  res0  5601  resres  5613  xpssres  5636  dfima2  5678  imai  5688  ima0  5691  imaundir  5757  xpima  5787  dmresv  5804  rescnvcnv  5808  dmtpop  5823  rnsnopg  5826  resdmres  5839  dmmpt  5844  dmco  5857  co01  5864  suc0  6012  unisuc  6014  iunsuc  6020  fresaun  6290  dffv4  6405  fvssunirn  6437  f1ossf1o  6618  fpr  6645  fvsnun2  6674  mpt20  6955  dmoprab  6971  rnoprab  6973  elrnmpt2res  7004  ov6g  7028  1st0  7404  2nd0  7405  dfmpt2  7501  curry1  7503  curry2  7506  fpar  7515  algrflem  7520  dftpos2  7604  tposoprab  7623  tposmpt2  7624  fvmpt2curryd  7632  wfrlem14  7664  wfrlem16  7666  dfrecs3  7705  tfrlem8  7716  seqomlem3  7783  df2o3  7810  omxpenlem  8300  dfsdom2  8322  marypha2lem2  8581  sup00  8609  epinid0  8744  scottexs  8997  scott0s  8998  infxpenc2  9128  kmlem3  9259  cdaassen  9289  ackbij1lem2  9328  compsscnv  9478  fin1a2lem12  9518  mulerpqlem  10062  1lt2nq  10080  axi2m1  10265  2p2e4  11427  numsuc  11773  numsucc  11799  decmul10add  11828  5p5e10  11830  6p4e10  11831  7p3e10  11834  xnegmnf  12259  pnfaddmnf  12279  fz0tp  12664  fz0to3un2pr  12665  fzo13pr  12776  fzo0to2pr  12777  fzo0to3tp  12778  fzo0to42pr  12779  fzo1to4tp  12780  sq4e2t8  13185  i4  13190  crreczi  13212  fac1  13284  fac3  13287  hashkf  13339  hashinf  13342  dmhashres  13349  hashun3  13391  cshwsexa  13794  dmtrclfv  13982  abs0  14248  absi  14249  trirecip  14817  geoihalfsum  14835  esum  15031  tan0  15101  coshval  15105  ef01bndlem  15134  3dvds  15275  3dvdsdec  15276  3dvds2dec  15277  sadc0  15395  3lcm2e6woprm  15547  6lcm4e12  15548  lcmf0  15566  prmo0  15957  gcdmodi  15995  karatsuba  16005  43prm  16040  139prm  16042  631prm  16045  1259lem1  16049  1259lem2  16050  1259lem3  16051  1259lem4  16052  1259lem5  16053  2503lem1  16055  2503lem2  16056  2503lem3  16057  4001lem1  16059  4001lem2  16060  4001lem3  16061  4001lem4  16062  ndxarg  16093  setsfun  16104  setsfun0  16105  xpsc  16422  pmtrsn  18140  psgnprfval1  18143  sylow2a  18235  0frgp  18393  ablfac1eu  18674  sralem  19386  opsrtoslem2  19693  ply1plusgfvi  19820  pf1rcl  19921  restcld  21190  neitr  21198  txbasval  21623  txindis  21651  cnmpt1st  21685  cnmpt2nd  21686  ufildr  21948  restmetu  22588  cphipval2  23252  reust  23381  ismbl  23507  mbfimaopnlem  23636  itg10  23669  itg2cnlem2  23743  itgz  23761  dvmptid  23934  cos2pi  24443  tan4thpi  24481  sincos6thpi  24482  pige3  24484  dfrelog  24526  logm1  24549  dvlog  24611  efopnlem2  24617  cxpexp  24628  root1id  24709  ang180lem2  24754  1cubrlem  24782  quart1  24797  atandm2  24818  efiasin  24829  asinsinlem  24832  asinsin  24833  asin1  24835  acos1  24836  atancj  24851  atanlogsublem  24856  efiatan2  24858  2efiatan  24859  tanatan  24860  dvatan  24876  log2cnv  24885  log2ublem2  24888  log2ublem3  24889  basellem8  25028  cht1  25105  chp1  25107  ppi1i  25108  ppi2i  25109  cht2  25112  cht3  25113  bclbnd  25219  bposlem8  25230  2lgslem3c  25337  2lgslem3d  25338  ax5seglem7  26029  axlowdimlem8  26043  axlowdimlem11  26046  vtxvalsnop  26147  iedgvalsnop  26148  umgrislfupgrlem  26231  usgrexmpledg  26370  usgredgffibi  26432  vdegp1bi  26661  edginwlk  26758  uhgrwkspthlem2  26878  wlksnwwlknvbijOLD  27046  clwwlkvbij  27282  clwwlkvbijOLDOLD  27283  clwwlkvbijOLD  27284  wlk2v2elem2  27329  frgrwopreglem3  27489  ex-dif  27611  ex-xp  27624  ex-rn  27628  ex-lcm  27646  ex-prmo  27647  ip0i  28008  ip1ilem  28009  ipdirilem  28012  ipasslem10  28022  hvnegdii  28247  hvaddcani  28250  hvsubaddi  28251  hisubcomi  28289  normlem0  28294  normlem3  28297  normlem9  28303  bcseqi  28305  norm0  28313  norm-ii-i  28322  norm3difi  28332  normpari  28339  normpar2i  28341  polid2i  28342  shs0i  28636  chj0i  28642  pjsslem  28866  ho0subi  28982  hoaddsubi  29008  hosd1i  29009  hopncani  29011  nmop0  29173  nmfn0  29174  lnopunilem1  29197  lnophmlem2  29204  opsqrlem2  29328  pjclem1  29382  atabsi  29588  dmdbr6ati  29610  inin  29677  iuninc  29704  gtiso  29805  f1od2  29826  fpwrelmapffs  29836  dfdec100  29903  dp20u  29911  dp3mul10  29931  dpmul1000  29932  dpexpp1  29941  dpadd2  29943  dpmul  29946  dpmul4  29947  1mhdrd  29949  lmat22det  30213  ordtcnvNEW  30291  ordtrest2NEW  30294  zlmtset  30334  qqhucn  30361  zrhre  30388  qqhre  30389  esumnul  30435  mbfmcst  30646  carsggect  30705  eulerpartgbij  30759  eulerpartlemn  30768  fib0  30786  fib1  30787  fib2  30789  fib3  30790  fib4  30791  fib5  30792  fib6  30793  0rrv  30838  coinflipprob  30866  ballotlem2  30875  ballotth  30924  signsvf0  30982  itgexpif  31009  hgt750lem  31054  hgt750lem2  31055  bnj1416  31430  derang0  31474  subfac0  31482  subfac1  31483  mthmpps  31802  problem2  31882  quad3  31886  dfrdg2  32021  trpred0  32056  noetalem2  32185  noetalem3  32186  pprodcnveq  32311  dffv5  32352  fullfunfv  32375  ellines  32580  rankeq1o  32599  onint1  32765  bj-xpimasn  33252  bj-pr11val  33303  bj-pr21val  33311  bj-pr22val  33317  bj-nuliotaALT  33330  bj-dfmpt2a  33382  icorempt2  33515  finxpreclem4  33547  finxp2o  33552  finxp3o  33553  matunitlindf  33720  poimirlem5  33727  poimirlem22  33744  poimirlem26  33748  poimirlem30  33752  ismblfin  33763  dvtan  33772  asindmre  33807  dvasin  33808  dvacos  33809  areacirclem5  33816  heiborlem6  33926  xrnres4  34476  dfcoels  34498  coss0  34542  refsymrels2  34624  hdmap1cbv  37583  sqn5ii  37747  diophrw  37824  dnwech  38119  lmhmlnmsplit  38158  fgraphopab  38289  arearect  38301  areaquad  38302  dmnonrel  38396  imanonrel  38399  cononrel1  38400  cononrel2  38401  rclexi  38422  dfrtrcl5  38436  cnvtrrel  38462  dfrcl2  38466  dfrcl4  38468  iunrelexp0  38494  comptiunov2i  38498  relexpaddss  38510  brtrclfv2  38519  trclfvdecomr  38520  corcltrcl  38531  cotrclrcl  38534  fsovcnvlem  38807  neicvgnvo  38913  hashnzfz  39019  lhe4.4ex1a  39028  disjinfi  39869  tgqioo2  40254  sumnnodd  40342  limsup0  40406  limsup10ex  40485  liminf10ex  40486  cosnegpi  40558  itgsin0pilem1  40645  stoweidlem13  40709  wallispilem4  40764  wallispi2lem1  40767  wallispi2lem2  40768  stirlinglem3  40772  dirkertrigeqlem1  40794  fourierdlem56  40858  fourierdlem57  40859  fourierdlem58  40860  fourierdlem62  40864  fourierdlem103  40905  fourierdlem104  40906  fourierdlem112  40914  sqwvfoura  40924  fouriersw  40927  etransclem23  40953  etransclem36  40966  etransclem38  40968  carageniuncllem1  41217  0ome  41225  ovn02  41264  smflimlem4  41464  smflim  41467  smflim2  41494  smflimsup  41516  smfliminf  41519  fmtno0  42027  fmtno1  42028  fmtno2  42037  fmtno3  42038  fmtno4  42039  fmtno5lem4  42043  139prmALT  42086  31prm  42087  5tcu2e40  42107  3exp4mod41  42108  41prothprmlem2  42110  41prothprm  42111  nnsum3primesgbe  42255  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbtbndlem1  42268  tgoldbachlt  42279  cznrnglem  42521  2t6m3t4e0  42694  zlmodzxzldeplem3  42859  sec0  43072