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  3133  un23  3364  in32  3417  dfrab2  3480  difun2  3572  tpidm23  3770  unisn  3907  dfiunv2  4004  uniop  4346  suc0  4506  unisuc  4508  iunsuc  4515  xpun  4785  dfrn2  4916  dfdmf  4922  dfrnf  4971  res0  5015  resres  5023  xpssres  5046  dfima2  5076  imai  5090  ima0  5093  imaundir  5148  xpima1  5181  xpima2m  5182  dmresv  5193  rescnvcnv  5197  dmtpop  5210  rnsnopg  5213  resdmres  5226  dmmpt  5230  dmco  5243  co01  5249  fpr  5831  fmptpr  5841  fvsnun2  5847  mpo0  6086  dmoprab  6097  rnoprab  6099  ov6g  6155  1st0  6302  2nd0  6303  dfmpo  6383  algrflem  6389  dftpos2  6422  tposoprab  6441  tposmpo  6442  tfrlem8  6479  frecsuc  6568  df2o3  6592  sbthlemi5  7151  sup00  7193  casedm  7276  djudm  7295  axi2m1  8085  2p2e4  9260  numsuc  9614  numsucc  9640  decmul10add  9669  5p5e10  9671  6p4e10  9672  7p3e10  9675  xnegmnf  10054  pnfaddmnf  10075  fz0tp  10347  fz0to3un2pr  10348  fzo0to2pr  10453  fzo0to3tp  10454  fzo0to42pr  10455  0tonninf  10692  1tonninf  10693  inftonninf  10694  sq4e2t8  10889  i4  10894  fac1  10981  fac3  10984  abs0  11609  absi  11610  trirecip  12052  geoihalfsum  12073  esum  12213  tan0  12282  ef01bndlem  12307  3dvds  12415  3dvdsdec  12416  3dvds2dec  12417  3lcm2e6woprm  12648  6lcm4e12  12649  gcdmodi  12984  karatsuba  12993  ennnfonelem1  13018  ndxarg  13095  setsfun  13107  setsfun0  13108  txbasval  14981  cnmpt1st  15002  cnmpt2nd  15003  dvmptidcn  15428  cos2pi  15518  tan4thpi  15555  sincos6thpi  15556  sqrt2cxp2logb9e3  15689  2lgslem3c  15814  2lgslem3d  15815  012of  16528  2o01f  16529  pwf1oexmid  16536  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592