Theorem 3eqtri 2255

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

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

This theorem is referenced by:  csbid  3134  un23  3365  in32  3418  dfrab2  3481  difun2  3573  tpidm23  3771  unisn  3908  dfiunv2  4005  uniop  4347  suc0  4507  unisuc  4509  iunsuc  4516  xpun  4786  dfrn2  4917  dfdmf  4923  dfrnf  4972  res0  5016  resres  5024  xpssres  5047  dfima2  5077  imai  5091  ima0  5094  imaundir  5149  xpima1  5182  xpima2m  5183  dmresv  5194  rescnvcnv  5198  dmtpop  5211  rnsnopg  5214  resdmres  5227  dmmpt  5231  dmco  5244  co01  5250  fpr  5836  fmptpr  5846  fvsnun2  5852  mpo0  6093  dmoprab  6104  rnoprab  6106  ov6g  6162  1st0  6309  2nd0  6310  dfmpo  6390  algrflem  6396  dftpos2  6429  tposoprab  6448  tposmpo  6449  tfrlem8  6486  frecsuc  6575  df2o3  6599  sbthlemi5  7162  sup00  7204  casedm  7287  djudm  7306  axi2m1  8097  2p2e4  9272  numsuc  9626  numsucc  9652  decmul10add  9681  5p5e10  9683  6p4e10  9684  7p3e10  9687  xnegmnf  10066  pnfaddmnf  10087  fz0tp  10359  fz0to3un2pr  10360  fzo0to2pr  10466  fzo0to3tp  10467  fzo0to42pr  10468  0tonninf  10705  1tonninf  10706  inftonninf  10707  sq4e2t8  10902  i4  10907  fac1  10994  fac3  10997  abs0  11638  absi  11639  trirecip  12082  geoihalfsum  12103  esum  12243  tan0  12312  ef01bndlem  12337  3dvds  12445  3dvdsdec  12446  3dvds2dec  12447  3lcm2e6woprm  12678  6lcm4e12  12679  gcdmodi  13014  karatsuba  13023  ennnfonelem1  13048  ndxarg  13125  setsfun  13137  setsfun0  13138  txbasval  15017  cnmpt1st  15038  cnmpt2nd  15039  dvmptidcn  15464  cos2pi  15554  tan4thpi  15591  sincos6thpi  15592  sqrt2cxp2logb9e3  15725  2lgslem3c  15850  2lgslem3d  15851  012of  16650  2o01f  16651  pwf1oexmid  16658  isomninnlem  16696  iswomninnlem  16716  ismkvnnlem  16719