Theorem 3eqtri 2165

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

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  csbid  3015  un23  3240  in32  3293  dfrab2  3356  difun2  3447  tpidm23  3632  unisn  3760  dfiunv2  3857  uniop  4185  suc0  4341  unisuc  4343  iunsuc  4350  xpun  4608  dfrn2  4735  dfdmf  4740  dfrnf  4788  res0  4831  resres  4839  xpssres  4862  dfima2  4891  imai  4903  ima0  4906  imaundir  4960  xpima1  4993  xpima2m  4994  dmresv  5005  rescnvcnv  5009  dmtpop  5022  rnsnopg  5025  resdmres  5038  dmmpt  5042  dmco  5055  co01  5061  fpr  5610  fmptpr  5620  fvsnun2  5626  mpo0  5849  dmoprab  5860  rnoprab  5862  ov6g  5916  1st0  6050  2nd0  6051  dfmpo  6128  algrflem  6134  dftpos2  6166  tposoprab  6185  tposmpo  6186  tfrlem8  6223  frecsuc  6312  df2o3  6335  sbthlemi5  6857  sup00  6898  casedm  6979  djudm  6998  axi2m1  7707  2p2e4  8871  numsuc  9219  numsucc  9245  decmul10add  9274  5p5e10  9276  6p4e10  9277  7p3e10  9280  xnegmnf  9642  pnfaddmnf  9663  fz0tp  9932  fzo0to2pr  10026  fzo0to3tp  10027  fzo0to42pr  10028  0tonninf  10243  1tonninf  10244  inftonninf  10245  sq4e2t8  10421  i4  10426  fac1  10507  fac3  10510  abs0  10862  absi  10863  trirecip  11302  geoihalfsum  11323  esum  11405  tan0  11474  ef01bndlem  11499  3dvdsdec  11598  3dvds2dec  11599  3lcm2e6woprm  11803  6lcm4e12  11804  ennnfonelem1  11956  ndxarg  12021  setsfun  12033  setsfun0  12034  txbasval  12475  cnmpt1st  12496  cnmpt2nd  12497  dvmptidcn  12886  cos2pi  12933  tan4thpi  12970  sincos6thpi  12971  sqrt2cxp2logb9e3  13100  012of  13363  2o01f  13364  pwf1oexmid  13367  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419