Theorem 3eqtri 2230

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  csbid  3101  un23  3332  in32  3385  dfrab2  3448  difun2  3540  tpidm23  3734  unisn  3866  dfiunv2  3963  uniop  4301  suc0  4459  unisuc  4461  iunsuc  4468  xpun  4737  dfrn2  4867  dfdmf  4872  dfrnf  4920  res0  4964  resres  4972  xpssres  4995  dfima2  5025  imai  5039  ima0  5042  imaundir  5097  xpima1  5130  xpima2m  5131  dmresv  5142  rescnvcnv  5146  dmtpop  5159  rnsnopg  5162  resdmres  5175  dmmpt  5179  dmco  5192  co01  5198  fpr  5768  fmptpr  5778  fvsnun2  5784  mpo0  6017  dmoprab  6028  rnoprab  6030  ov6g  6086  1st0  6232  2nd0  6233  dfmpo  6311  algrflem  6317  dftpos2  6349  tposoprab  6368  tposmpo  6369  tfrlem8  6406  frecsuc  6495  df2o3  6518  sbthlemi5  7065  sup00  7107  casedm  7190  djudm  7209  axi2m1  7990  2p2e4  9165  numsuc  9519  numsucc  9545  decmul10add  9574  5p5e10  9576  6p4e10  9577  7p3e10  9580  xnegmnf  9953  pnfaddmnf  9974  fz0tp  10246  fz0to3un2pr  10247  fzo0to2pr  10349  fzo0to3tp  10350  fzo0to42pr  10351  0tonninf  10587  1tonninf  10588  inftonninf  10589  sq4e2t8  10784  i4  10789  fac1  10876  fac3  10879  abs0  11402  absi  11403  trirecip  11845  geoihalfsum  11866  esum  12006  tan0  12075  ef01bndlem  12100  3dvds  12208  3dvdsdec  12209  3dvds2dec  12210  3lcm2e6woprm  12441  6lcm4e12  12442  gcdmodi  12777  karatsuba  12786  ennnfonelem1  12811  ndxarg  12888  setsfun  12900  setsfun0  12901  txbasval  14772  cnmpt1st  14793  cnmpt2nd  14794  dvmptidcn  15219  cos2pi  15309  tan4thpi  15346  sincos6thpi  15347  sqrt2cxp2logb9e3  15480  2lgslem3c  15605  2lgslem3d  15606  012of  15967  2o01f  15968  pwf1oexmid  15973  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028