Theorem 3eqtri 2256

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

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

This theorem is referenced by:  csbid  3136  un23  3368  in32  3421  dfrab2  3484  difun2  3576  if0ab  3610  tpidm23  3776  unisn  3914  dfiunv2  4011  uniop  4354  suc0  4514  unisuc  4516  iunsuc  4523  xpun  4793  dfrn2  4924  dfdmf  4930  dfrnf  4979  res0  5023  resres  5031  xpssres  5054  dfima2  5084  imai  5099  ima0  5102  imaundir  5157  xpima1  5190  xpima2m  5191  dmresv  5202  rescnvcnv  5206  dmtpop  5219  rnsnopg  5222  resdmres  5235  dmmpt  5239  dmco  5252  co01  5258  fpr  5844  fmptpr  5854  fvsnun2  5860  mpo0  6101  dmoprab  6112  rnoprab  6114  ov6g  6170  1st0  6316  2nd0  6317  dfmpo  6397  algrflem  6403  dftpos2  6470  tposoprab  6489  tposmpo  6490  tfrlem8  6527  frecsuc  6616  df2o3  6640  sbthlemi5  7203  sup00  7262  casedm  7345  djudm  7364  axi2m1  8155  2p2e4  9329  numsuc  9685  numsucc  9711  decmul10add  9740  5p5e10  9742  6p4e10  9743  7p3e10  9746  xnegmnf  10125  pnfaddmnf  10146  fz0tp  10419  fz0to3un2pr  10420  fzo0to2pr  10526  fzo0to3tp  10527  fzo0to42pr  10528  0tonninf  10765  1tonninf  10766  inftonninf  10767  sq4e2t8  10962  i4  10967  fac1  11054  fac3  11057  abs0  11698  absi  11699  trirecip  12142  geoihalfsum  12163  esum  12303  tan0  12372  ef01bndlem  12397  3dvds  12505  3dvdsdec  12506  3dvds2dec  12507  3lcm2e6woprm  12738  6lcm4e12  12739  gcdmodi  13074  karatsuba  13083  ennnfonelem1  13108  ndxarg  13185  setsfun  13197  setsfun0  13198  txbasval  15078  cnmpt1st  15099  cnmpt2nd  15100  dvmptidcn  15525  cos2pi  15615  tan4thpi  15652  sincos6thpi  15653  sqrt2cxp2logb9e3  15786  2lgslem3c  15914  2lgslem3d  15915  012of  16713  2o01f  16714  pwf1oexmid  16721  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785