Theorem 3eqtri 2256

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  csbid  3135  un23  3366  in32  3419  dfrab2  3482  difun2  3574  tpidm23  3772  unisn  3909  dfiunv2  4006  uniop  4348  suc0  4508  unisuc  4510  iunsuc  4517  xpun  4787  dfrn2  4918  dfdmf  4924  dfrnf  4973  res0  5017  resres  5025  xpssres  5048  dfima2  5078  imai  5092  ima0  5095  imaundir  5150  xpima1  5183  xpima2m  5184  dmresv  5195  rescnvcnv  5199  dmtpop  5212  rnsnopg  5215  resdmres  5228  dmmpt  5232  dmco  5245  co01  5251  fpr  5835  fmptpr  5845  fvsnun2  5851  mpo0  6090  dmoprab  6101  rnoprab  6103  ov6g  6159  1st0  6306  2nd0  6307  dfmpo  6387  algrflem  6393  dftpos2  6426  tposoprab  6445  tposmpo  6446  tfrlem8  6483  frecsuc  6572  df2o3  6596  sbthlemi5  7159  sup00  7201  casedm  7284  djudm  7303  axi2m1  8094  2p2e4  9269  numsuc  9623  numsucc  9649  decmul10add  9678  5p5e10  9680  6p4e10  9681  7p3e10  9684  xnegmnf  10063  pnfaddmnf  10084  fz0tp  10356  fz0to3un2pr  10357  fzo0to2pr  10462  fzo0to3tp  10463  fzo0to42pr  10464  0tonninf  10701  1tonninf  10702  inftonninf  10703  sq4e2t8  10898  i4  10903  fac1  10990  fac3  10993  abs0  11618  absi  11619  trirecip  12061  geoihalfsum  12082  esum  12222  tan0  12291  ef01bndlem  12316  3dvds  12424  3dvdsdec  12425  3dvds2dec  12426  3lcm2e6woprm  12657  6lcm4e12  12658  gcdmodi  12993  karatsuba  13002  ennnfonelem1  13027  ndxarg  13104  setsfun  13116  setsfun0  13117  txbasval  14990  cnmpt1st  15011  cnmpt2nd  15012  dvmptidcn  15437  cos2pi  15527  tan4thpi  15564  sincos6thpi  15565  sqrt2cxp2logb9e3  15698  2lgslem3c  15823  2lgslem3d  15824  012of  16592  2o01f  16593  pwf1oexmid  16600  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656