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  5836  fmptpr  5846  fvsnun2  5852  mpo0  6091  dmoprab  6102  rnoprab  6104  ov6g  6160  1st0  6307  2nd0  6308  dfmpo  6388  algrflem  6394  dftpos2  6427  tposoprab  6446  tposmpo  6447  tfrlem8  6484  frecsuc  6573  df2o3  6597  sbthlemi5  7160  sup00  7202  casedm  7285  djudm  7304  axi2m1  8095  2p2e4  9270  numsuc  9624  numsucc  9650  decmul10add  9679  5p5e10  9681  6p4e10  9682  7p3e10  9685  xnegmnf  10064  pnfaddmnf  10085  fz0tp  10357  fz0to3un2pr  10358  fzo0to2pr  10464  fzo0to3tp  10465  fzo0to42pr  10466  0tonninf  10703  1tonninf  10704  inftonninf  10705  sq4e2t8  10900  i4  10905  fac1  10992  fac3  10995  abs0  11636  absi  11637  trirecip  12080  geoihalfsum  12101  esum  12241  tan0  12310  ef01bndlem  12335  3dvds  12443  3dvdsdec  12444  3dvds2dec  12445  3lcm2e6woprm  12676  6lcm4e12  12677  gcdmodi  13012  karatsuba  13021  ennnfonelem1  13046  ndxarg  13123  setsfun  13135  setsfun0  13136  txbasval  15010  cnmpt1st  15031  cnmpt2nd  15032  dvmptidcn  15457  cos2pi  15547  tan4thpi  15584  sincos6thpi  15585  sqrt2cxp2logb9e3  15718  2lgslem3c  15843  2lgslem3d  15844  012of  16643  2o01f  16644  pwf1oexmid  16651  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708