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  4300  suc0  4458  unisuc  4460  iunsuc  4467  xpun  4736  dfrn2  4866  dfdmf  4871  dfrnf  4919  res0  4963  resres  4971  xpssres  4994  dfima2  5024  imai  5038  ima0  5041  imaundir  5096  xpima1  5129  xpima2m  5130  dmresv  5141  rescnvcnv  5145  dmtpop  5158  rnsnopg  5161  resdmres  5174  dmmpt  5178  dmco  5191  co01  5197  fpr  5766  fmptpr  5776  fvsnun2  5782  mpo0  6015  dmoprab  6026  rnoprab  6028  ov6g  6084  1st0  6230  2nd0  6231  dfmpo  6309  algrflem  6315  dftpos2  6347  tposoprab  6366  tposmpo  6367  tfrlem8  6404  frecsuc  6493  df2o3  6516  sbthlemi5  7063  sup00  7105  casedm  7188  djudm  7207  axi2m1  7988  2p2e4  9163  numsuc  9517  numsucc  9543  decmul10add  9572  5p5e10  9574  6p4e10  9575  7p3e10  9578  xnegmnf  9951  pnfaddmnf  9972  fz0tp  10244  fz0to3un2pr  10245  fzo0to2pr  10347  fzo0to3tp  10348  fzo0to42pr  10349  0tonninf  10585  1tonninf  10586  inftonninf  10587  sq4e2t8  10782  i4  10787  fac1  10874  fac3  10877  abs0  11369  absi  11370  trirecip  11812  geoihalfsum  11833  esum  11973  tan0  12042  ef01bndlem  12067  3dvds  12175  3dvdsdec  12176  3dvds2dec  12177  3lcm2e6woprm  12408  6lcm4e12  12409  gcdmodi  12744  karatsuba  12753  ennnfonelem1  12778  ndxarg  12855  setsfun  12867  setsfun0  12868  txbasval  14739  cnmpt1st  14760  cnmpt2nd  14761  dvmptidcn  15186  cos2pi  15276  tan4thpi  15313  sincos6thpi  15314  sqrt2cxp2logb9e3  15447  2lgslem3c  15572  2lgslem3d  15573  012of  15930  2o01f  15931  pwf1oexmid  15936  isomninnlem  15969  iswomninnlem  15988  ismkvnnlem  15991