Theorem 3eqtri 2257

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 2253	. 2 |- B = D
5	1, 4	eqtri 2253	1 |- A = D

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  csbid  3146  un23  3378  in32  3433  dfrab2  3496  difun2  3589  if0ab  3623  tpidm23  3792  unisn  3930  dfiunv2  4027  uniop  4372  suc0  4532  unisuc  4534  iunsuc  4541  xpun  4811  dfrn2  4943  dfdmf  4949  dfrnf  4998  res0  5042  resres  5050  xpssres  5073  dfima2  5103  imai  5118  ima0  5121  imaundir  5176  xpima1  5209  xpima2m  5210  dmresv  5221  rescnvcnv  5225  dmtpop  5238  rnsnopg  5241  resdmres  5254  dmmpt  5258  dmco  5271  co01  5277  fpr  5866  fmptpr  5876  fvsnun2  5882  mpo0  6123  dmoprab  6134  rnoprab  6136  ov6g  6192  1st0  6338  2nd0  6339  dfmpo  6419  algrflem  6425  dftpos2  6492  tposoprab  6511  tposmpo  6512  tfrlem8  6549  frecsuc  6638  df2o3  6662  sbthlemi5  7231  sup00  7294  casedm  7377  djudm  7396  axi2m1  8190  2p2e4  9364  numsuc  9722  numsucc  9748  decmul10add  9777  5p5e10  9779  6p4e10  9780  7p3e10  9783  xnegmnf  10162  pnfaddmnf  10183  fz0tp  10456  fz0to3un2pr  10457  fzo0to2pr  10563  fzo0to3tp  10564  fzo0to42pr  10565  0tonninf  10802  1tonninf  10803  inftonninf  10804  sq4e2t8  10999  i4  11004  fac1  11091  fac3  11094  abs0  11743  absi  11744  trirecip  12187  geoihalfsum  12208  esum  12348  tan0  12417  ef01bndlem  12442  3dvds  12550  3dvdsdec  12551  3dvds2dec  12552  3lcm2e6woprm  12783  6lcm4e12  12784  gcdmodi  13119  karatsuba  13128  ballotfilem2  13142  ennnfonelem1  13158  ndxarg  13235  setsfun  13247  setsfun0  13248  txbasval  15132  cnmpt1st  15153  cnmpt2nd  15154  dvmptidcn  15579  cos2pi  15669  tan4thpi  15706  sincos6thpi  15707  sqrt2cxp2logb9e3  15840  2lgslem3c  15968  2lgslem3d  15969  012of  16767  2o01f  16768  pwf1oexmid  16773  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837