Theorem 3eqtri 2113

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

Syntax hints:   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

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

This theorem is referenced by:  csbid  2941  un23  3160  in32  3213  dfrab2  3275  difun2  3366  tpidm23  3547  unisn  3675  dfiunv2  3772  uniop  4091  suc0  4247  unisuc  4249  iunsuc  4256  xpun  4512  dfrn2  4637  dfdmf  4642  dfrnf  4689  res0  4730  resres  4738  xpssres  4760  dfima2  4789  imai  4801  ima0  4804  imaundir  4858  xpima1  4890  xpima2m  4891  dmresv  4902  rescnvcnv  4906  dmtpop  4919  rnsnopg  4922  resdmres  4935  dmmpt  4939  dmco  4952  co01  4958  fpr  5493  fmptpr  5503  fvsnun2  5509  mpt20  5732  dmoprab  5743  rnoprab  5745  ov6g  5796  1st0  5929  2nd0  5930  dfmpt2  6002  algrflem  6008  dftpos2  6040  tposoprab  6059  tposmpt2  6060  tfrlem8  6097  frecsuc  6186  df2o3  6209  sbthlemi5  6724  sup00  6752  casedm  6831  djudm  6841  axi2m1  7471  2p2e4  8604  numsuc  8951  numsucc  8977  decmul10add  9006  5p5e10  9008  6p4e10  9009  7p3e10  9012  xnegmnf  9352  fz0tp  9596  fzo0to2pr  9690  fzo0to3tp  9691  fzo0to42pr  9692  0tonninf  9906  1tonninf  9907  inftonninf  9908  sq4e2t8  10113  i4  10118  fac1  10198  fac3  10201  abs0  10552  absi  10553  trirecip  10956  geoihalfsum  10977  esum  11013  tan0  11083  ef01bndlem  11108  3dvdsdec  11204  3dvds2dec  11205  3lcm2e6woprm  11407  6lcm4e12  11408  ndxarg  11578  setsfun  11590  setsfun0  11591