Theorem 3eqtri 2221

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbid  3092  un23  3322  in32  3375  dfrab2  3438  difun2  3530  tpidm23  3723  unisn  3855  dfiunv2  3952  uniop  4288  suc0  4446  unisuc  4448  iunsuc  4455  xpun  4724  dfrn2  4854  dfdmf  4859  dfrnf  4907  res0  4950  resres  4958  xpssres  4981  dfima2  5011  imai  5025  ima0  5028  imaundir  5083  xpima1  5116  xpima2m  5117  dmresv  5128  rescnvcnv  5132  dmtpop  5145  rnsnopg  5148  resdmres  5161  dmmpt  5165  dmco  5178  co01  5184  fpr  5744  fmptpr  5754  fvsnun2  5760  mpo0  5992  dmoprab  6003  rnoprab  6005  ov6g  6061  1st0  6202  2nd0  6203  dfmpo  6281  algrflem  6287  dftpos2  6319  tposoprab  6338  tposmpo  6339  tfrlem8  6376  frecsuc  6465  df2o3  6488  sbthlemi5  7027  sup00  7069  casedm  7152  djudm  7171  axi2m1  7942  2p2e4  9117  numsuc  9470  numsucc  9496  decmul10add  9525  5p5e10  9527  6p4e10  9528  7p3e10  9531  xnegmnf  9904  pnfaddmnf  9925  fz0tp  10197  fz0to3un2pr  10198  fzo0to2pr  10294  fzo0to3tp  10295  fzo0to42pr  10296  0tonninf  10532  1tonninf  10533  inftonninf  10534  sq4e2t8  10729  i4  10734  fac1  10821  fac3  10824  abs0  11223  absi  11224  trirecip  11666  geoihalfsum  11687  esum  11827  tan0  11896  ef01bndlem  11921  3dvds  12029  3dvdsdec  12030  3dvds2dec  12031  3lcm2e6woprm  12254  6lcm4e12  12255  gcdmodi  12590  karatsuba  12599  ennnfonelem1  12624  ndxarg  12701  setsfun  12713  setsfun0  12714  txbasval  14503  cnmpt1st  14524  cnmpt2nd  14525  dvmptidcn  14950  cos2pi  15040  tan4thpi  15077  sincos6thpi  15078  sqrt2cxp2logb9e3  15211  2lgslem3c  15336  2lgslem3d  15337  012of  15640  2o01f  15641  pwf1oexmid  15644  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696