Theorem 3eqtri 2263

Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)

Hypotheses

Ref	Expression
3eqtri.1	|- A = B
3eqtri.2	|- B = C
3eqtri.3	|- C = D

Assertion

Ref	Expression
3eqtri	|- A = D

Proof of Theorem 3eqtri

Step	Hyp	Ref	Expression
1		3eqtri.1	. 2 |- A = B
2		3eqtri.2	. . 3 |- B = C
3		3eqtri.3	. . 3 |- C = D
4	2, 3	eqtri 2259	. 2 |- B = D
5	1, 4	eqtri 2259	1 |- A = D

Syntax hints:   = wceq 1402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  csbid  3155  un23  3388  in32  3443  dfrab2  3508  dfnul4  3522  difun2  3604  if0ab  3638  tpidm23  3808  unisn  3946  dfiunv2  4043  uniop  4391  suc0  4551  unisuc  4553  iunsuc  4560  xpun  4831  dfrn2  4963  dfdmf  4969  dfrnf  5018  res0  5062  resres  5070  xpssres  5093  dfima2  5123  imai  5138  ima0  5141  imaundir  5196  xpima1  5229  xpima2m  5230  dmresv  5241  rescnvcnv  5245  dmtpop  5258  rnsnopg  5261  resdmres  5274  dmmpt  5278  dmco  5291  co01  5297  fpr  5888  fmptpr  5898  fvsnun2  5904  mpo0  6148  dmoprab  6159  rnoprab  6161  ov6g  6217  1st0  6368  2nd0  6369  dfmpo  6449  algrflem  6455  dftpos2  6522  tposoprab  6541  tposmpo  6542  tfrlem8  6579  frecsuc  6668  df2o3  6692  sbthlemi5  7268  sup00  7333  casedm  7416  djudm  7435  axi2m1  8232  2p2e4  9410  numsuc  9769  numsucc  9795  decmul10add  9824  5p5e10  9826  6p4e10  9827  7p3e10  9830  xnegmnf  10210  pnfaddmnf  10231  fz0tp  10507  fz0to3un2pr  10508  fzo0to2pr  10614  fzo0to3tp  10615  fzo0to42pr  10616  0tonninf  10855  1tonninf  10856  inftonninf  10857  sq4e2t8  11052  i4  11057  fac1  11145  fac3  11148  abs0  11802  absi  11803  trirecip  12246  geoihalfsum  12267  esum  12407  tan0  12476  ef01bndlem  12501  3dvds  12609  3dvdsdec  12610  3dvds2dec  12611  3lcm2e6woprm  12842  6lcm4e12  12843  gcdmodi  13178  karatsuba  13187  ballotfilem2  13206  ballotfilemth  13259  ennnfonelem1  13276  ndxarg  13353  setsfun  13365  setsfun0  13366  txbasval  15291  cnmpt1st  15312  cnmpt2nd  15313  dvmptidcn  15738  cos2pi  15828  tan4thpi  15865  sincos6thpi  15866  sqrt2cxp2logb9e3  16000  2lgslem3c  16128  2lgslem3d  16129  012of  16937  2o01f  16938  pwf1oexmid  16943  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007