Theorem 3eqtri 2259

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  csbid  3149  un23  3382  in32  3437  dfrab2  3500  difun2  3593  if0ab  3627  tpidm23  3797  unisn  3935  dfiunv2  4032  uniop  4377  suc0  4537  unisuc  4539  iunsuc  4546  xpun  4816  dfrn2  4948  dfdmf  4954  dfrnf  5003  res0  5047  resres  5055  xpssres  5078  dfima2  5108  imai  5123  ima0  5126  imaundir  5181  xpima1  5214  xpima2m  5215  dmresv  5226  rescnvcnv  5230  dmtpop  5243  rnsnopg  5246  resdmres  5259  dmmpt  5263  dmco  5276  co01  5282  fpr  5871  fmptpr  5881  fvsnun2  5887  mpo0  6131  dmoprab  6142  rnoprab  6144  ov6g  6200  1st0  6351  2nd0  6352  dfmpo  6432  algrflem  6438  dftpos2  6505  tposoprab  6524  tposmpo  6525  tfrlem8  6562  frecsuc  6651  df2o3  6675  sbthlemi5  7244  sup00  7307  casedm  7390  djudm  7409  axi2m1  8206  2p2e4  9381  numsuc  9740  numsucc  9766  decmul10add  9795  5p5e10  9797  6p4e10  9798  7p3e10  9801  xnegmnf  10181  pnfaddmnf  10202  fz0tp  10478  fz0to3un2pr  10479  fzo0to2pr  10585  fzo0to3tp  10586  fzo0to42pr  10587  0tonninf  10826  1tonninf  10827  inftonninf  10828  sq4e2t8  11023  i4  11028  fac1  11116  fac3  11119  abs0  11768  absi  11769  trirecip  12212  geoihalfsum  12233  esum  12373  tan0  12442  ef01bndlem  12467  3dvds  12575  3dvdsdec  12576  3dvds2dec  12577  3lcm2e6woprm  12808  6lcm4e12  12809  gcdmodi  13144  karatsuba  13153  ballotfilem2  13172  ballotfilemth  13225  ennnfonelem1  13242  ndxarg  13319  setsfun  13331  setsfun0  13332  txbasval  15258  cnmpt1st  15279  cnmpt2nd  15280  dvmptidcn  15705  cos2pi  15795  tan4thpi  15832  sincos6thpi  15833  sqrt2cxp2logb9e3  15966  2lgslem3c  16094  2lgslem3d  16095  012of  16893  2o01f  16894  pwf1oexmid  16899  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963