Theorem 3eqtri 2254

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbid  3132  un23  3363  in32  3416  dfrab2  3479  difun2  3571  tpidm23  3767  unisn  3904  dfiunv2  4001  uniop  4342  suc0  4502  unisuc  4504  iunsuc  4511  xpun  4780  dfrn2  4910  dfdmf  4916  dfrnf  4965  res0  5009  resres  5017  xpssres  5040  dfima2  5070  imai  5084  ima0  5087  imaundir  5142  xpima1  5175  xpima2m  5176  dmresv  5187  rescnvcnv  5191  dmtpop  5204  rnsnopg  5207  resdmres  5220  dmmpt  5224  dmco  5237  co01  5243  fpr  5821  fmptpr  5831  fvsnun2  5837  mpo0  6074  dmoprab  6085  rnoprab  6087  ov6g  6143  1st0  6290  2nd0  6291  dfmpo  6369  algrflem  6375  dftpos2  6407  tposoprab  6426  tposmpo  6427  tfrlem8  6464  frecsuc  6553  df2o3  6576  sbthlemi5  7128  sup00  7170  casedm  7253  djudm  7272  axi2m1  8062  2p2e4  9237  numsuc  9591  numsucc  9617  decmul10add  9646  5p5e10  9648  6p4e10  9649  7p3e10  9652  xnegmnf  10025  pnfaddmnf  10046  fz0tp  10318  fz0to3un2pr  10319  fzo0to2pr  10424  fzo0to3tp  10425  fzo0to42pr  10426  0tonninf  10662  1tonninf  10663  inftonninf  10664  sq4e2t8  10859  i4  10864  fac1  10951  fac3  10954  abs0  11569  absi  11570  trirecip  12012  geoihalfsum  12033  esum  12173  tan0  12242  ef01bndlem  12267  3dvds  12375  3dvdsdec  12376  3dvds2dec  12377  3lcm2e6woprm  12608  6lcm4e12  12609  gcdmodi  12944  karatsuba  12953  ennnfonelem1  12978  ndxarg  13055  setsfun  13067  setsfun0  13068  txbasval  14941  cnmpt1st  14962  cnmpt2nd  14963  dvmptidcn  15388  cos2pi  15478  tan4thpi  15515  sincos6thpi  15516  sqrt2cxp2logb9e3  15649  2lgslem3c  15774  2lgslem3d  15775  012of  16357  2o01f  16358  pwf1oexmid  16365  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420