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  5825  fmptpr  5835  fvsnun2  5841  mpo0  6080  dmoprab  6091  rnoprab  6093  ov6g  6149  1st0  6296  2nd0  6297  dfmpo  6375  algrflem  6381  dftpos2  6413  tposoprab  6432  tposmpo  6433  tfrlem8  6470  frecsuc  6559  df2o3  6583  sbthlemi5  7139  sup00  7181  casedm  7264  djudm  7283  axi2m1  8073  2p2e4  9248  numsuc  9602  numsucc  9628  decmul10add  9657  5p5e10  9659  6p4e10  9660  7p3e10  9663  xnegmnf  10037  pnfaddmnf  10058  fz0tp  10330  fz0to3un2pr  10331  fzo0to2pr  10436  fzo0to3tp  10437  fzo0to42pr  10438  0tonninf  10674  1tonninf  10675  inftonninf  10676  sq4e2t8  10871  i4  10876  fac1  10963  fac3  10966  abs0  11585  absi  11586  trirecip  12028  geoihalfsum  12049  esum  12189  tan0  12258  ef01bndlem  12283  3dvds  12391  3dvdsdec  12392  3dvds2dec  12393  3lcm2e6woprm  12624  6lcm4e12  12625  gcdmodi  12960  karatsuba  12969  ennnfonelem1  12994  ndxarg  13071  setsfun  13083  setsfun0  13084  txbasval  14957  cnmpt1st  14978  cnmpt2nd  14979  dvmptidcn  15404  cos2pi  15494  tan4thpi  15531  sincos6thpi  15532  sqrt2cxp2logb9e3  15665  2lgslem3c  15790  2lgslem3d  15791  012of  16444  2o01f  16445  pwf1oexmid  16452  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508